src/HOL/Set.thy
changeset 5931 325300576da7
parent 5780 0187f936685a
child 7238 36e58620ffc8
equal deleted inserted replaced
5930:41aa67a045f7 5931:325300576da7
    37   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
    37   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
    38   "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
    38   "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
    39   (*membership*)
    39   (*membership*)
    40   "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    40   "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    41 
    41 
    42 
       
    43 (*For compatibility: DELETE after one release*)
       
    44 syntax Compl :: ('a set) => 'a set   (*complement*)
       
    45 translations "Compl A"  => "- A"
       
    46 
    42 
    47 (** Additional concrete syntax **)
    43 (** Additional concrete syntax **)
    48 
    44 
    49 syntax
    45 syntax
    50 
    46