[isabelle-dev] New HOL/Import
makarius at sketis.net
Thu Mar 29 20:04:26 CEST 2012
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:
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?
More information about the isabelle-dev