src/HOL/Set.thy
changeset 5492 d9fc3457554e
parent 5254 a275d0a3dc08
child 5780 0187f936685a
     1.1 --- a/src/HOL/Set.thy	Tue Sep 15 15:06:29 1998 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Sep 15 15:10:38 1998 +0200
     1.3 @@ -28,7 +28,6 @@
     1.4    UNIV          :: 'a set
     1.5    insert        :: ['a, 'a set] => 'a set
     1.6    Collect       :: ('a => bool) => 'a set               (*comprehension*)
     1.7 -  Compl         :: ('a set) => 'a set                   (*complement*)
     1.8    Int           :: ['a set, 'a set] => 'a set       (infixl 70)
     1.9    Un            :: ['a set, 'a set] => 'a set       (infixl 65)
    1.10    UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
    1.11 @@ -41,11 +40,15 @@
    1.12    "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    1.13  
    1.14  
    1.15 +(*For compatibility: DELETE after one release*)
    1.16 +syntax Compl :: ('a set) => 'a set   (*complement*)
    1.17 +translations "Compl A"  => "- A"
    1.18  
    1.19  (** Additional concrete syntax **)
    1.20  
    1.21  syntax
    1.22  
    1.23 +
    1.24    (* Infix syntax for non-membership *)
    1.25  
    1.26    "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    1.27 @@ -144,7 +147,7 @@
    1.28    Bex_def       "Bex A P        == ? x. x:A & P(x)"
    1.29    subset_def    "A <= B         == ! x:A. x:B"
    1.30    psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
    1.31 -  Compl_def     "Compl A        == {x. ~x:A}"
    1.32 +  Compl_def     "- A            == {x. ~x:A}"
    1.33    Un_def        "A Un B         == {x. x:A | x:B}"
    1.34    Int_def       "A Int B        == {x. x:A & x:B}"
    1.35    set_diff_def  "A - B          == {x. x:A & ~x:B}"