[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
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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