Re: [isabelle] Status of HOL/Import
On Wed, 13 Jul 2011, Cezary Kaliszyk wrote:
It does work now.
To build it one needs the proof objects from HOL-Light.
I did not expect this to happen so quickly.
I packed the ones generated from the current version at:
(Archive is 13Mb, but it takes nearly 1Gb after extracting).
It reminds me again of the setup from 2004/2005 for HOL4. If this is not
becoming part of one of the automated tests in the background, it will not
last very long.
If you extract it so the files are in:
do "export HOL4_PROOFS=~/tmp"
before running "isabelle make HOL-Generate-HOLLight"
Better use Isabelle settings for such things -- as was done in 2004
This archive was generated by a fusion of
Pipermail (Mailman edition) and