src/HOL/Set.thy
changeset 1068 e0f2dffab506
parent 923 ff1574a81019
child 1273 6960ec882bca
     1.1 --- a/src/HOL/Set.thy	Sat Apr 22 12:21:41 1995 +0200
     1.2 +++ b/src/HOL/Set.thy	Sat Apr 22 13:25:31 1995 +0200
     1.3 @@ -41,20 +41,20 @@
     1.4  
     1.5    "@Finset"     :: "args => 'a set"                   ("{(_)}")
     1.6  
     1.7 -  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")
     1.8 +  "@Coll"       :: "[pttrn, bool] => 'a set"          ("(1{_./ _})")
     1.9    "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
    1.10  
    1.11    (* Big Intersection / Union *)
    1.12  
    1.13 -  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
    1.14 -  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
    1.15 +  "@INTER"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
    1.16 +  "@UNION"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
    1.17  
    1.18    (* Bounded Quantifiers *)
    1.19  
    1.20 -  "@Ball"       :: "[idt, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
    1.21 -  "@Bex"        :: "[idt, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
    1.22 -  "*Ball"       :: "[idt, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
    1.23 -  "*Bex"        :: "[idt, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
    1.24 +  "@Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
    1.25 +  "@Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
    1.26 +  "*Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
    1.27 +  "*Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
    1.28  
    1.29  translations
    1.30    "x ~: y"      == "~ (x : y)"