Quoting Makarius <makar...@sketis.net>:
On Fri, 12 Apr 2013, Clemens Ballarin wrote:
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.
I am aware of the modularity aspect of this. My criticism is that
deviations from the current approach in favour of preferable notation
are not even considered. In any case, I'm not sure how useful the old
notation still is. Maybe it can be given up at some point.
Clemens
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev