diff -r d199410f1db1 -r 968d2dccf2de Set.thy
--- a/Set.thy	Mon Oct 04 15:43:54 1993 +0100
+++ b/Set.thy	Thu Oct 07 10:20:30 1993 +0100
@@ -19,20 +19,20 @@
 
   (* Constants *)
 
-  Collect       :: "('a => bool) => 'a set"               (*comprehension*)
-  Compl         :: "('a set) => 'a set"                   (*complement*)
-  Int           :: "['a set, 'a set] => 'a set"       (infixl 70)
-  Un            :: "['a set, 'a set] => 'a set"       (infixl 65)
-  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"     (*general*)
-  UNION1        :: "['a => 'b set] => 'b set"         (binder "UN " 10)
-  INTER1        :: "['a => 'b set] => 'b set"         (binder "INT " 10)
-  Union, Inter  :: "(('a set)set) => 'a set"              (*of a set*)
-  range         :: "('a => 'b) => 'b set"                 (*of function*)
-  Ball, Bex     :: "['a set, 'a => bool] => bool"         (*bounded quantifiers*)
-  inj, surj     :: "('a => 'b) => bool"                   (*injective/surjective*)
+  Collect       :: "('a => bool) => 'a set"             (*comprehension*)
+  Compl         :: "('a set) => 'a set"                 (*complement*)
+  Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
+  Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
+  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"   (*general*)
+  UNION1        :: "['a => 'b set] => 'b set"           (binder "UN " 10)
+  INTER1        :: "['a => 'b set] => 'b set"           (binder "INT " 10)
+  Union, Inter  :: "(('a set)set) => 'a set"            (*of a set*)
+  range         :: "('a => 'b) => 'b set"               (*of function*)
+  Ball, Bex     :: "['a set, 'a => bool] => bool"       (*bounded quantifiers*)
+  inj, surj     :: "('a => 'b) => bool"                 (*inj/surjective*)
   inj_onto      :: "['a => 'b, 'a set] => bool"
-  "``"          :: "['a => 'b, 'a set] => ('b set)"   (infixl 90)
-  ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
+  "``"          :: "['a => 'b, 'a set] => ('b set)"     (infixl 90)
+  ":", "~:"	:: "['a, 'a set] => bool" (infixl 50)   (*membership*)
 
   (* Finite Sets *)
 
@@ -43,7 +43,7 @@
 
   (** Binding Constants **)
 
-  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")  (*collection*)
+  "@Coll"       :: "[idt, bool] => 'a set"   ("(1{_./ _})")  (*collection*)
 
   (* Big Intersection / Union *)
 
@@ -67,6 +67,8 @@
   "ALL x:A. P"  => "Ball(A, %x. P)"
   "EX x:A. P"   => "Bex(A, %x. P)"
 
+  "x ~: y"      == "~ (x:y)"
+
   "{x, xs}"     == "insert(x, {xs})"
   "{x}"         == "insert(x, {})"