On Wed, 17 Apr 2013, Clemens Ballarin wrote:
Quoting Makarius <makar...@sketis.net>:
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
In any case, I'm not sure how useful the old notation still is. Maybe it
can be given up at some point.
(Clearing out old mail threads, I've come across this again.)
Does it mean you propose to discontinue "(in a)" at some point?
An old idea on my list is to add some support to the Prover IDE to rework
theories with many consecutive "(in a)" to use just one "context a begin
... end" around it -- this is also more efficient. Apart from that I have
occasionally considered to provide explicit fold support for such contexts
in the editor -- the canonical layout does not have any indentation here.
Thus "(in a)" would eventually become more rare in practice, although my
speculations did not go as far as discontinuing it altogether. It might
be worth to reconsider that question at some point nonetheless.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
