[isabelle-dev] New HOL/Import

[Makarius]

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