src/HOL/Set.thy

--- a/src/HOL/Set.thy	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/Set.thy	Wed Nov 18 15:10:46 1998 +0100
@@ -40,10 +40,6 @@
   "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
 
 
-(*For compatibility: DELETE after one release*)
-syntax Compl :: ('a set) => 'a set   (*complement*)
-translations "Compl A"  => "- A"
-
 (** Additional concrete syntax **)
 
 syntax