Hello Isabelle developers.
I'm doing an experiment in which I need to programmatically construct a locale.
For simplicity I used the same operations that Michael Norrish was using in the
l4.verified C code parser, Local_Theory.define and Local_Theory.notes. This led
to some strange behaviour.
On Thu, 7 Apr 2011, Thomas Sewell wrote:
Suppose I set up ML actions for adding a definition foo = True to a
locale and for getting the constant named foo
locale test = assumes True
begin
ML {*
val add_foo = Local_Theory.define ((@{binding foo}, NoSyn),
(Attrib.empty_binding, @{term True}))
