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

[Tobias Nipkow]

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?
>>
>>
>> Thanks,
>>
>>
>> Norbert.
>>
>>
>>
>>
>>
>>
>>