[isabelle-dev] [isabelle] Status of HOL/Import
florian.haftmann at informatik.tu-muenchen.de
Sun Mar 4 10:15:38 CET 2012
I've been working on the Importer stuff, not very deeply, but separating
HOL4 and HOL Light contents, stripping generic parts of any name
reference to HOL4, etc. The visible change is that most parts can now
be directly edited using jEdit, which is the base for any further
I do not claim that the naming terminology I have invented is the best
(it surely isn't), but now it should not be difficult to improve it, in
There could be done a lot more on the ML stuff to introduce basic coding
practice there, of course, but for the moment I will leave that aside.
a) There is a README; maybe you would like to update it according to
your current expertise?
b) After the pred/set issue, the generated HOL Light theories must be
regenerated. Do you have time to accomplish this? Alternatively, I
could follow the README instructions as soon as available.
And, n.b.: HOL4_PROOFS is now named IMPORTER_PROOFS.
> However there is still the question of what to do with the HOL4
> import; as the old exporter
> seems to be lost and I don't think people are interested in writing a new one...
Well, keep it »as it is« at the moment… ;-)
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev