Importing HOL into Isabelle/HOL

Steven Obua, Sebastian Skalberg

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Is- abelle/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.
Original languageEnglish
Title of host publicationAutomated Reasoning
Subtitle of host publicationThird International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings
EditorsUlrich Furbach, Natarajan Shankar
PublisherSpringer Berlin Heidelberg
Number of pages5
ISBN (Electronic)978-3-540-37188-5
ISBN (Print)978-3-540-37187-8
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Cite this