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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
