[isabelle] HOL4 building problem resolved

The problem with building HOL4 is caused by the importer expecting the
import specification tables in the current working directory.  The
easiest way to circumvent this is to use a prebuilt HOL4 image as
follows (Isabelle 2008):

* switch to the HOL directory
* then issue

	isatool make HOL4

* then select the HOL4 image in the Isabelle/Logics menu of proof general
* import HOL4 in your theory header

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.