[isabelle-dev] New HOL/Import

[Makarius]

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