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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
