src/HOL/Set.thy
changeset 5931 325300576da7
parent 5780 0187f936685a
child 7238 36e58620ffc8
     1.1 --- a/src/HOL/Set.thy	Wed Nov 18 11:12:29 1998 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Nov 18 15:10:46 1998 +0100
     1.3 @@ -40,10 +40,6 @@
     1.4    "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
     1.5  
     1.6  
     1.7 -(*For compatibility: DELETE after one release*)
     1.8 -syntax Compl :: ('a set) => 'a set   (*complement*)
     1.9 -translations "Compl A"  => "- A"
    1.10 -
    1.11  (** Additional concrete syntax **)
    1.12  
    1.13  syntax