diff -r a52f53caf424 -r 72754e060aa2 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 23 17:46:12 1996 +0200
+++ b/src/HOL/Set.thy	Mon Sep 23 17:47:49 1996 +0200
@@ -32,14 +32,16 @@
   inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
   inj_onto      :: ['a => 'b, 'a set] => bool
   "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
-  ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)
+     (*membership*)
+  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50,51] 50)
 
 
 syntax
 
   UNIV         :: 'a set
 
-  "~:"          :: ['a, 'a set] => bool             (infixl 50)
+     (*infix synatx for non-membership*)
+  "op ~:"        :: ['a, 'a set] => bool             ("(_/ ~: _)" [50,51] 50)
 
   "@Finset"     :: args => 'a set                   ("{(_)}")