Sciweavers

CADE
2006
Springer
14 years 5 months ago
An Interpretation of Isabelle/HOL in HOL Light
We define an interpretation of the Isabelle/HOL logic in HOL Light and its metalanguage, OCaml. Some aspects of the Isabelle logic are not representable directly in the HOL Light o...
Sean McLaughlin