On Thu, Mar 29, 2012 at 8:04 PM, Makarius <makar...@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 magnitude bigger. >> - 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? Regards, Cezary _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev