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