[isabelle-dev] Testing HOL/Import
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