src/HOL/Set.thy
changeset 1370 7361ac9b024d
parent 1273 6960ec882bca
child 1531 e5eb247ad13c
     1.1 --- a/src/HOL/Set.thy	Mon Nov 27 13:44:56 1995 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Nov 29 16:44:59 1995 +0100
     1.3 @@ -16,45 +16,45 @@
     1.4    set :: (term) {ord, minus}
     1.5  
     1.6  consts
     1.7 -  "{}"          :: "'a set"                           ("{}")
     1.8 -  insert        :: "['a, 'a set] => 'a set"
     1.9 -  Collect       :: "('a => bool) => 'a set"               (*comprehension*)
    1.10 -  Compl         :: "('a set) => 'a set"                   (*complement*)
    1.11 -  Int           :: "['a set, 'a set] => 'a set"       (infixl 70)
    1.12 -  Un            :: "['a set, 'a set] => 'a set"       (infixl 65)
    1.13 -  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"     (*general*)
    1.14 -  UNION1        :: "['a => 'b set] => 'b set"         (binder "UN " 10)
    1.15 -  INTER1        :: "['a => 'b set] => 'b set"         (binder "INT " 10)
    1.16 -  Union, Inter  :: "(('a set)set) => 'a set"              (*of a set*)
    1.17 -  Pow           :: "'a set => 'a set set"                 (*powerset*)
    1.18 -  range         :: "('a => 'b) => 'b set"                 (*of function*)
    1.19 -  Ball, Bex     :: "['a set, 'a => bool] => bool"         (*bounded quantifiers*)
    1.20 -  inj, surj     :: "('a => 'b) => bool"                   (*inj/surjective*)
    1.21 -  inj_onto      :: "['a => 'b, 'a set] => bool"
    1.22 -  "``"          :: "['a => 'b, 'a set] => ('b set)"   (infixl 90)
    1.23 -  ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
    1.24 +  "{}"          :: 'a set                           ("{}")
    1.25 +  insert        :: ['a, 'a set] => 'a set
    1.26 +  Collect       :: ('a => bool) => 'a set               (*comprehension*)
    1.27 +  Compl         :: ('a set) => 'a set                   (*complement*)
    1.28 +  Int           :: ['a set, 'a set] => 'a set       (infixl 70)
    1.29 +  Un            :: ['a set, 'a set] => 'a set       (infixl 65)
    1.30 +  UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
    1.31 +  UNION1        :: ['a => 'b set] => 'b set         (binder "UN " 10)
    1.32 +  INTER1        :: ['a => 'b set] => 'b set         (binder "INT " 10)
    1.33 +  Union, Inter  :: (('a set)set) => 'a set              (*of a set*)
    1.34 +  Pow           :: 'a set => 'a set set                 (*powerset*)
    1.35 +  range         :: ('a => 'b) => 'b set                 (*of function*)
    1.36 +  Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
    1.37 +  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
    1.38 +  inj_onto      :: ['a => 'b, 'a set] => bool
    1.39 +  "``"          :: ['a => 'b, 'a set] => ('b set)   (infixl 90)
    1.40 +  ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)
    1.41  
    1.42  
    1.43  syntax
    1.44  
    1.45 -  "~:"          :: "['a, 'a set] => bool"             (infixl 50)
    1.46 +  "~:"          :: ['a, 'a set] => bool             (infixl 50)
    1.47  
    1.48 -  "@Finset"     :: "args => 'a set"                   ("{(_)}")
    1.49 +  "@Finset"     :: args => 'a set                   ("{(_)}")
    1.50  
    1.51 -  "@Coll"       :: "[pttrn, bool] => 'a set"          ("(1{_./ _})")
    1.52 -  "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
    1.53 +  "@Coll"       :: [pttrn, bool] => 'a set          ("(1{_./ _})")
    1.54 +  "@SetCompr"   :: ['a, idts, bool] => 'a set       ("(1{_ |/_./ _})")
    1.55  
    1.56    (* Big Intersection / Union *)
    1.57  
    1.58 -  "@INTER"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
    1.59 -  "@UNION"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
    1.60 +  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
    1.61 +  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
    1.62  
    1.63    (* Bounded Quantifiers *)
    1.64  
    1.65 -  "@Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
    1.66 -  "@Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
    1.67 -  "*Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
    1.68 -  "*Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
    1.69 +  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" 10)
    1.70 +  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" 10)
    1.71 +  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" 10)
    1.72 +  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" 10)
    1.73  
    1.74  translations
    1.75    "x ~: y"      == "~ (x : y)"