--- a/src/ZF/zf.thy Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/zf.thy Thu Oct 07 10:48:16 1993 +0100
@@ -100,6 +100,7 @@
" ->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*)
"<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
":" :: "[i, i] => o" (infixl 50) (*membership relation*)
+ "~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)
translations
@@ -124,6 +125,8 @@
"ALL x:A. P" == "Ball(A, %x. P)"
"EX x:A. P" == "Bex(A, %x. P)"
+ "x ~: y" == "~ (x:y)"
+
rules
@@ -145,7 +148,7 @@
infinity "0:Inf & (ALL y:Inf. succ(y): Inf)"
(*This formulation facilitates case analysis on A. *)
-foundation "A=0 | (EX x:A. ALL y:x. ~ y:A)"
+foundation "A=0 | (EX x:A. ALL y:x. y~:A)"
(* Schema axiom since predicate P is a higher-order variable *)
replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \