[isabelle] ZF theory - loading problem



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.