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