Sciweavers

CADE
2006
Springer
14 years 5 months ago
Importing HOL into Isabelle/HOL
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 a...
Steven Obua, Sebastian Skalberg