[isabelle-dev] Interpretation in arbitrary targets.

Makarius makarius at sketis.net
Fri Apr 12 22:08:18 CEST 2013

On Fri, 12 Apr 2013, Clemens Ballarin wrote:

>> foo (in l) ...
>> is equivalent to
>> context l
>> begin
>> foo ...
>> end
>> by construction.  We cannot have just one of them.
> That sounds a bit dogmatic.  If additional commands are made available for 
> targets, then the syntax should clearly be more flexible if better intuition 
> can be achieved.

That is just a matter of modularity of concepts: the older "(in a)" 
notation was slightly generalized at some point to allow named contexts as 
sketched above, and the relation between the two is as pointed out by 

A "localized" Isar command does not see the difference, since this is 
managed uniformly by the toplevel.


More information about the isabelle-dev mailing list