[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Makarius <makarius at sketis.net>:

> On Fri, 12 Apr 2013, Clemens Ballarin wrote:
>
>> That sounds a bit dogmatic.  If additional commands are made  
>> available for targets, then the syntax should clearly be more  
>> flexible if better intuition can be achieved.
>
> 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, and the relation between the two is as  
> pointed out by Florian.

I am aware of the modularity aspect of this.  My criticism is that  
deviations from the current approach in favour of preferable notation  
are not even considered.  In any case, I'm not sure how useful the old  
notation still is.  Maybe it can be given up at some point.

Clemens