Re: [isabelle] ZF theory - loading problem



It sounds like you are trying to load parts of Isabelle/ZF on top of Isabelle/HOL. These are entirely separate instantiations of Isabelle. To use Isabelle/ZF, launch Isabelle jEdit and look for the menu (top right on the screen) that says âdefault (HOL)â. Now select ZF. This should build Isabelle/ZF, including all its constituent theories.

Larry Paulson


> On 18 Apr 2016, at 14:30, Omar Jasim <oajasim1 at sheffield.ac.uk> wrote:
> 
> Hi
> 
> Please I have problem with loading ZF theory in Isabelle 2016 as I was
> tring to load Order.thy to use it in my work (I trid it in Isabelle 2015
> and its working properly). I tired to load all the ZF corresponding
> theories such as HOL - ZF, ZF-AC, ZF- coins , ZF-IMP, etc. But the problem
> still. When I load the ZF theory I there appear a problems in:
> definition function :: "i â o" â ârecognizes functions; can have non-pairsâ
> where "function(r) == âx y. âx,yâ â r â (ây'. âx,y'â â r â y = y')"
> definition Pi :: "[i, i â i] â i" where "Pi(A,B) == {fâPow(Sigma(A,B)).
> Aâdomain(f) & function(f)}"
> and many other problems
> So any one know what going on?
> 
> Omar





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.