[isabelle-dev] Testing HOL/Import
bulwahn at in.tum.de
Wed Jul 20 21:39:35 CEST 2011
On 07/20/2011 09:34 PM, Florian Haftmann wrote:
> Dear all,
>> with Cezary's guidance, I set up mira configurations for building the
>> proofs bundle from the HOL Light repository and for running the
>> HOL-Generate-HOLLight with that bundle, cf.
>> for the first successful run. I experienced some fairly reproducible
>> segmentation faults on some machines, but lxbroy5-9 seem to work. This
>> is still prior to Cezary's major cleanup in 6ca79a354c51, so there is
>> hope for improvements here.
> these are good news, thanks for the excellent work that is going on!
> A humble question: is there any chance that also the HOL4 import can be
As we discussed at lunch in Munich, we have an expert on HOL4, Thomas
Tuerk, who might take that opportunity.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev