[isabelle-dev] Interpretation in arbitrary targets.
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
More information about the isabelle-dev