[isabelle-dev] Interpretation in arbitrary targets.
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
>> foo ...
>> 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