[isabelle-dev] Testing HOL/Import

[Makarius]

On Wed, 20 Jul 2011, Lukas Bulwahn wrote:

>> A humble question:  is there any chance that also the HOL4 import can 
>> be covered?
>> 
> As we discussed at lunch in Munich, we have an expert on HOL4, Thomas 
> Tuerk, who might take that opportunity.

Just FYI: some old HOL4 proofs are here

   /home/isabelle/dist/dist-Isabelle2005/contrib/HOL4-proofs.tar.gz


 	Makarius