On Tue, 8 Jan 2013, Florian Haftmann wrote:
This is a left-over from the isabelle build reform from last summer: Do
the additional HOL images still have a purpose? Notably:
HOL-Base
HOL-Plain
HOL-Main
If HOL-Plain vanished, the same could apply to Plain.thy itself.
That is a different question, one about the internal organization of the
HOL session. I did not dare to raise it here, since I no longer
understand it sufficiently to have an informed opinion on it.
Historically, we had introduced Plain as a stepping stone where all
definitional packages are already bootstrapped, and thus a reasonably safe
ground to start some minimal applications. Before Plain it used to be
Arith or PreList. Now we have many packages bootstrapped after Plain, and
the PreList syndrome can be avoided by changing the canonical introductory
example slightly -- see my version of it here
http://www.lri.fr/~wenzel/Isabelle_Orleans_2012/Seq.thy
Experts on HOL's structure are welcome to reconsider it eventually. For
the release we should not open that can, though.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
