[isabelle-dev] New HOL/Import
krauss at in.tum.de
Mon Apr 2 00:07:01 CEST 2012
On 03/28/2012 11:33 PM, Cezary Kaliszyk wrote:
> We have been working on a modernized reimplementation of HOL/Import,
> for HOL Light. We think we are at a point where it could be pushed to
> the main Isabelle repository replacing the old one.
This has happened now, cf. 4c7548e7df86.
A component with a proof bundle exported from HOL Light (and
postprocessed further) is available at
It contains HOL-Light's equivalent of "Main", i.e., the lemmas that you
get when you use "hol.ml" in HOL Light. When this component is
available, it will be imported as part of the HOL-Import session. You'll
know that it happens when that session takes 30 seconds to run instead
of 3 (on my laptop).
Of course, this is not the whole story, as we are actually targeting
flyspeck :-) Further refinements will happen at some point: we'll be
looking at parallelization, and also try to track down remaining
More information about the isabelle-dev