[isabelle-dev] New HOL/Import

Cezary Kaliszyk cezarykaliszyk at gmail.com
Wed Mar 28 23:33:27 CEST 2012

Hi all,

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 mailing list