[isabelle-dev] Purpose of additional HOL images

[Makarius]

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