On 10/03/16 11:19, Makarius wrote:
> On Thu, 10 Mar 2016, Johannes Hölzl wrote:
>
>> Alternatively: Would a lattice_syntax locale work nowadays? I remember
>> I tried it once and for some reason it didn't work. Either notations
>> aren't supported in locales or they are exported after the context
*** General ***
* Command 'bundle' provides a local theory target to define a bundle
from the body of specification commands (such as 'declare',
'declaration', 'notation', 'lemmas', 'lemma'). For example:
bundle foo
begin
declare a [simp]
declare b [intro]
end
* Command 'unbundle' is like
