[isabelle-dev] Interpretation in arbitrary targets.

[Makarius]

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 
Florian.

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


 	Makarius