Re: [isabelle] Status of HOL/Import

On Tue, Jul 12, 2011 at 5:15 PM, Alexander Krauss <krauss at> wrote:
>> Is anyone using HOL/Import or the theorems translated from HOLLight
>> or can I update the generation and compatibility scripts to work
>> with current Isabelle and svn HOLLight, add some constant maps
>> and update the generated theorems?
> If you manage to revive the whole thing go ahead. But we should extend the
> regression test as soon as it works again.

It does work now.
To build it one needs the proof objects from HOL-Light.

I packed the ones generated from the current version at:

(Archive is 13Mb, but it takes nearly 1Gb after extracting).

If you extract it so the files are in:

do "export HOL4_PROOFS=~/tmp"

before running "isabelle make HOL-Generate-HOLLight"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.