[isabelle-dev] New HOL/Import

[Alexander Krauss]

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

 
http://isabelle.in.tum.de/devel/components/hol-light-bundle-0.5-126.tar.gz

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 
bottlenecks.

Alex