[isabelle-dev] ZF and HOL in same session?

[Alexander Krauss]

At the moment, HOL and ZF developments can be loaded in the same 
session, but they cannot be merged, i.e. no theory can import both of 
them. But one can potentially transfer results from one development to 
the other by translating proofs.

Alex


Tobias Nipkow wrote:
> We are experimenting with transferring results from HOL to ZF.
> 
> Tobias
> 
> Lawrence Paulson schrieb:
>> Unfortunately I don't know the answer to this. I have copied this 
>> message to the developers mailing list and maybe somebody else can 
>> help you.
>> Larry
>>
>> On 21 Aug 2008, at 11:02, Norbert Voelker wrote:
>>
>>> Larry/Tobias,
>>>
>>>
>>> the Isabelle2008 News contain the following intriguing sentence:
>>>
>>>
>>> * Renamed some theories to allow to loading both ZF and HOL in the 
>>> same session:
>>>
>>>
>>> I would be interested to hear more about this. Does it mean that 
>>> there is now (or in future) a possible integration between HOL and 
>>> ZF,  such as access to the ZF types i/o from within a HOL framework?