Email Gateway (Aug 22 2022 at 13:10): Email Gateway (Aug 22 2022 at 13:10):From: Omar Jasim <oajasim1@sheffield.ac.uk>
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
Email Gateway (Aug 22 2022 at 13:10):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: Apr 25 2024 at 08:20 UTC