src/ZF/ZF.thy

   "Un"  :: "[i, i] => i"         (infixl 65) (*binary union*)
   "-"   :: "[i, i] => i"         (infixl 65) (*set difference*)
   " ->" :: "[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
   "{x, xs}"     == "cons(x, {xs})"
   "{x}"         == "cons(x, 0)"

   "THE x. P"    == "The(%x. P)"
   "lam x:A. f"  == "Lambda(A, %x. f)"
   "ALL x:A. P"  == "Ball(A, %x. P)"
   "EX x:A. P"   == "Bex(A, %x. P)"
 
+  "x ~: y"      == "~ (x:y)"
+
 
 rules
 
  (* Bounded Quantifiers *)
 Ball_def        "Ball(A,P) == ALL x. x:A --> P(x)"

 
  (*We may name this set, though it is not uniquely defined. *)
 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) ==> \
 \                        b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"