[isabelle-dev] New HOL/Import

[Cezary Kaliszyk]

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:
   http://cl-informatik.uibk.ac.at/~cek/import.html
   http://cl-informatik.uibk.ac.at/~cek/import.pdf

 - The code is shorter and cleaner.

For those that would like to inspect the code it is at:
  http://cl-informatik.uibk.ac.at/~cek/import.tgz

Regards,

Cezary

-- 
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/~cek/