Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOL4 building problem resolved

Email Gateway (Aug 18 2022 at 12:44):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc

Last updated: May 03 2024 at 12:27 UTC