[isabelle-dev] [isabelle] Status of HOL/Import

[Florian Haftmann]

Hi Cezary,

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
refinement.

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
case.

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.

Two questions:
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… ;-)

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120304/db4fe986/attachment.asc>