[isabelle-dev] Named target renovation

[Makarius]

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 
release.


 	Makarius