[isabelle-dev] Testing HOL/Import

Makarius makarius at sketis.net
Mon Jul 25 14:27:12 CEST 2011

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



More information about the isabelle-dev mailing list