src/HOL/Set.thy

 consts
   "{}"          :: 'a set                           ("{}")
   UNIV          :: 'a set
   insert        :: ['a, 'a set] => 'a set
   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*)
   Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
   Pow           :: 'a set => 'a set set                 (*powerset*)

   "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
   (*membership*)
   "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
+
 
   (* Infix syntax for non-membership *)
 
   "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
   "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)

 
   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   Bex_def       "Bex A P        == ? x. x:A & P(x)"
   subset_def    "A <= B         == ! x:A. x:B"
   psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
-  Compl_def     "Compl A        == {x. ~x:A}"
+  Compl_def     "- A            == {x. ~x:A}"
   Un_def        "A Un B         == {x. x:A | x:B}"
   Int_def       "A Int B        == {x. x:A & x:B}"
   set_diff_def  "A - B          == {x. x:A & ~x:B}"
   INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
   UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"