Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

8

CADE
2006
Springer

favoriteEmaildiscussreport

129views Logical Reasoning» more CADE 2006»

Importing HOL into Isabelle/HOL

14 years 4 months ago

Importing HOL into Isabelle/HOL

Download www4.in.tum.de

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.

Steven Obua, Sebastian Skalberg

Real-time Traffic

Automated Reasoning | CADE 2006 | Source Hol System |

claim paper

Related Content

» Formalizing O Notation in IsabelleHOL

» An Interpretation of IsabelleHOL in HOL Light

» Quotients revisited for IsabelleHOL

» Proof of the Basic Theorem on Concept Lattices in IsabelleHOL

» HigherOrder Abstract Syntax in IsabelleHOL

» Extracting a Normalization Algorithm in IsabelleHOL

» Craigs Interpolation Theorem formalised and mechanised in IsabelleHOL

» Unifying Theories in IsabelleHOL

» A Recursion Combinator for Nominal Datatypes Implemented in IsabelleHOL

Post Info
More Details (n/a)

Added	03 Dec 2009
Updated	03 Dec 2009
Type	Conference
Year	2006
Where	CADE
Authors	Steven Obua, Sebastian Skalberg

Comments (0)