Re: [isabelle] Status of HOL/Import
On Tue, Jul 12, 2011 at 5:15 PM, Alexander Krauss <krauss at in.tum.de> 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