[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Makarius <makarius at sketis.net>:

> Does it mean you propose to discontinue "(in a)" at some point?

Exactly.  Too early right now, but eventually this might make sense --  
especially if the IDE provides suitable refactorings.  Of course, this  
wouldn't let us scrap a lot of code, but the Isar language could  
become cleaner.

Clemens