[isabelle-dev] Purpose of additional HOL images
makarius at sketis.net
Wed Jan 9 12:00:51 CET 2013
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:
> 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
Experts on HOL's structure are welcome to reconsider it eventually. For
the release we should not open that can, though.
More information about the isabelle-dev