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

[Lawrence Paulson]

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.
>
>
>
>
>
>
>