We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Isabelle/HOL that have been recorded in HOL 4 or HOL-light and is therefore completely safe. Concepts in the source HOL system, that is types and constants, can be mapped to concepts in Isabelle/HOL; this facilitates a true integration of imported theorems and theorems that are already available in Isabelle/HOL. The importer is part of the standard Isabelle distribution.
Full Text: Importing HOL into Isabelle/HOL [pdf] (accepted for IJCAR 2006)
Supplementary Material:
HOL 4 proof objects [tar.gz], HOL-light proof objects [tar.gz]
Java Implementation of HOL-light kernel + Importer: binary [jar], source [tar.gz]
An Abstract HOL-Kernel [pdf] (preliminary notes)
Last update: April 29th 2006, 4:00 PM.