[isabelle-dev] Interpretation in arbitrary targets.

Clemens Ballarin ballarin at in.tum.de
Tue May 21 19:45:23 CEST 2013

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.


More information about the isabelle-dev mailing list