[isabelle-dev] New HOL/Import
cezarykaliszyk at gmail.com
Wed Mar 28 23:33:27 CEST 2012
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.
Therefore two questions:
- Is anyone using the old HOL/Import?
- Does anyone have opinions about the HOL4 code that has been long dead?
Most important changes in the new importer as opposed to the old one:
- It is much more scalable. Regular HOL-Light can be imported in
less than a minute. Importing bigger theories works as well.
- Rather than generating 'thy' files it creates an Image file and
documentation, see either of the below:
- The code is shorter and cleaner.
For those that would like to inspect the code it is at:
Cezary Kaliszyk, University of Innsbruck,
More information about the isabelle-dev