[isabelle-dev] Interpretation in arbitrary targets.

Lawrence Paulson lp15 at cam.ac.uk
Tue May 21 12:53:58 CEST 2013

Naturally this notation is less important than before, and never strictly essential. But would we save much by eliminating it?


On 21 May 2013, at 11:46, Makarius <makarius at 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.

More information about the isabelle-dev mailing list