On Wed, 28 Mar 2012, Cezary Kaliszyk wrote:
- 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
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.
You are no longer using any XML/YXML now. Is the format somehow related
to OpenTheory by Joe Hurd?
- Is anyone using the old HOL/Import?
In principle you could ask on isabelle-users as well, although I would be
surprised to hear about anybody using the old relic. It has sucked up
maintenance resources for many years, without tangible results.
- Does anyone have opinions about the HOL4 code that has been long dead?
Which HOL4 code do you mean exactly?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
