[isabelle-dev] Interpretation in arbitrary targets.

[Lawrence Paulson]

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 <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.