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