Naturally this notation is less important than before, and never strictly essential. But would we save much by eliminating it?
Larry On 21 May 2013, at 11:46, Makarius <makar...@sketis.net> wrote: > 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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
