On Wed, 28 Mar 2012, Cezary Kaliszyk wrote:
We have been working on a modernized reimplementation of HOL/Import,
for HOL Light. We think we are at a point where it could be pushed to
the main Isabelle repository
You know the formalities for that:
* Wiring in IsaMakefile for static part (ML etc), say with some
conditional loading of actual HOL_Light proofs (that blob cannot
be managed easily within the repository, so one can make a conditional
test as for some other sessions, depending on settings that
isatest/mira will provide.)
* Canonical file headers with authors etc.
* NEWS entry
* CONTRIBUTORS entry
replacing the old one.
I am not adressing this here. It depends on who answers your initial
question.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
