[isabelle-dev] Named target renovation

Makarius makarius at sketis.net
Tue Jul 1 21:27:01 CEST 2014

On Mon, 9 Jun 2014, Florian Haftmann wrote:

> To get a glimpse how things have evolved over time, see here the state 
> of the art in Isabelle2009-2 (still without nested local theories!)
> http://isabelle.in.tum.de/repos/isabelle/raw-file/35815ce9218a/src/Pure/Isar/theory_target.ML
> and now the current polished version
> http://isabelle.in.tum.de/repos/isabelle/raw-file/4cf607675df8/src/Pure/Isar/generic_target.ML
> http://isabelle.in.tum.de/repos/isabelle/raw-file/4cf607675df8/src/Pure/Isar/named_target.ML
> where any obscurity has vanished from named_target.ML (which goes back
> to the ancient theory_target.ML).

Direct comparison of the files is probably difficult, but I have followed 
most of the individual changesets.  So far it looks formally OK for the 


More information about the isabelle-dev mailing list