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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
