[isabelle-dev] Interpretation in arbitrary targets.

[Makarius]

On Wed, 17 Apr 2013, Clemens Ballarin wrote:

> Quoting Makarius <makarius at 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