[isabelle-dev] New HOL/Import
cezarykaliszyk at gmail.com
Thu Mar 29 23:21:13 CEST 2012
On Thu, Mar 29, 2012 at 8:04 PM, Makarius <makarius at sketis.net> wrote:
> Wow, I am impressed by the brevity of it. You should mention the secret
> http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be
> uncompressed, before it can be used with import_file in the example.
That's the preprocessed proof image for importing basic hol-light.
> You are no longer using any XML/YXML now. Is the format somehow related to
> OpenTheory by Joe Hurd?
No; the information stored is similar to the old format, but more brief and
easier to parse: every line contains a next typ/term/thm to read, with
arguments space separated and last uses of an object marked with a minus.
It could be converted (possibly automatically) to OpenTheory; however the
sharing is done at a different level so it would be hard to recover additional
sharing and without it, Opentheory would be at least an order of
>> - Does anyone have opinions about the HOL4 code that has been long dead?
> Which HOL4 code do you mean exactly?
The code currently in isabelle repository is in 3 places:
Import, Import/HOL_Light and Import/HOL4
The Import/HOL_Light is functional but the proposed code replaces it.
The Import/HOL4 has not been functional for a while, (I have not been able
to use it even with proofs from 2004); should it still stay in the repository?
More information about the isabelle-dev