src/HOL/HOL.thy
changeset 1370 7361ac9b024d
parent 1273 6960ec882bca
child 1672 2c109cd2fdd0
     1.1 --- a/src/HOL/HOL.thy	Mon Nov 27 13:44:56 1995 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Nov 29 16:44:59 1995 +0100
     1.3 @@ -35,33 +35,33 @@
     1.4  
     1.5    (* Constants *)
     1.6  
     1.7 -  Trueprop      :: "bool => prop"                     ("(_)" 5)
     1.8 -  not           :: "bool => bool"                     ("~ _" [40] 40)
     1.9 -  True, False   :: "bool"
    1.10 -  If            :: "[bool, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
    1.11 -  Inv           :: "('a => 'b) => ('b => 'a)"
    1.12 +  Trueprop      :: bool => prop                     ("(_)" 5)
    1.13 +  not           :: bool => bool                     ("~ _" [40] 40)
    1.14 +  True, False   :: bool
    1.15 +  If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    1.16 +  Inv           :: ('a => 'b) => ('b => 'a)
    1.17  
    1.18    (* Binders *)
    1.19  
    1.20 -  Eps           :: "('a => bool) => 'a"
    1.21 -  All           :: "('a => bool) => bool"             (binder "! " 10)
    1.22 -  Ex            :: "('a => bool) => bool"             (binder "? " 10)
    1.23 -  Ex1           :: "('a => bool) => bool"             (binder "?! " 10)
    1.24 -  Let           :: "['a, 'a => 'b] => 'b"
    1.25 +  Eps           :: ('a => bool) => 'a
    1.26 +  All           :: ('a => bool) => bool             (binder "! " 10)
    1.27 +  Ex            :: ('a => bool) => bool             (binder "? " 10)
    1.28 +  Ex1           :: ('a => bool) => bool             (binder "?! " 10)
    1.29 +  Let           :: ['a, 'a => 'b] => 'b
    1.30  
    1.31    (* Infixes *)
    1.32  
    1.33 -  o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl 55)
    1.34 -  "="           :: "['a, 'a] => bool"                 (infixl 50)
    1.35 -  "&"           :: "[bool, bool] => bool"             (infixr 35)
    1.36 -  "|"           :: "[bool, bool] => bool"             (infixr 30)
    1.37 -  "-->"         :: "[bool, bool] => bool"             (infixr 25)
    1.38 +  o             :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    1.39 +  "="           :: ['a, 'a] => bool                 (infixl 50)
    1.40 +  "&"           :: [bool, bool] => bool             (infixr 35)
    1.41 +  "|"           :: [bool, bool] => bool             (infixr 30)
    1.42 +  "-->"         :: [bool, bool] => bool             (infixr 25)
    1.43  
    1.44    (* Overloaded Constants *)
    1.45  
    1.46 -  "+"           :: "['a::plus, 'a] => 'a"             (infixl 65)
    1.47 -  "-"           :: "['a::minus, 'a] => 'a"            (infixl 65)
    1.48 -  "*"           :: "['a::times, 'a] => 'a"            (infixl 70)
    1.49 +  "+"           :: ['a::plus, 'a] => 'a             (infixl 65)
    1.50 +  "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
    1.51 +  "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.52  
    1.53  
    1.54  types
    1.55 @@ -70,29 +70,29 @@
    1.56  
    1.57  syntax
    1.58  
    1.59 -  "~="          :: "['a, 'a] => bool"                 (infixl 50)
    1.60 +  "~="          :: ['a, 'a] => bool                 (infixl 50)
    1.61  
    1.62 -  "@Eps"        :: "[pttrn,bool] => 'a"               ("(3@ _./ _)" 10)
    1.63 +  "@Eps"        :: [pttrn,bool] => 'a               ("(3@ _./ _)" 10)
    1.64  
    1.65    (* Alternative Quantifiers *)
    1.66  
    1.67 -  "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
    1.68 -  "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)
    1.69 -  "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" 10)
    1.70 +  "*All"        :: [idts, bool] => bool             ("(3ALL _./ _)" 10)
    1.71 +  "*Ex"         :: [idts, bool] => bool             ("(3EX _./ _)" 10)
    1.72 +  "*Ex1"        :: [idts, bool] => bool             ("(3EX! _./ _)" 10)
    1.73  
    1.74    (* Let expressions *)
    1.75  
    1.76 -  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
    1.77 -  ""            :: "letbind => letbinds"              ("_")
    1.78 -  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
    1.79 -  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
    1.80 +  "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
    1.81 +  ""            :: letbind => letbinds              ("_")
    1.82 +  "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
    1.83 +  "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
    1.84  
    1.85    (* Case expressions *)
    1.86  
    1.87 -  "@case"       :: "['a, cases_syn] => 'b"            ("(case _ of/ _)" 10)
    1.88 -  "@case1"      :: "['a, 'b] => case_syn"             ("(2_ =>/ _)" 10)
    1.89 -  ""            :: "case_syn => cases_syn"            ("_")
    1.90 -  "@case2"      :: "[case_syn, cases_syn] => cases_syn"   ("_/ | _")
    1.91 +  "@case"       :: ['a, cases_syn] => 'b            ("(case _ of/ _)" 10)
    1.92 +  "@case1"      :: ['a, 'b] => case_syn             ("(2_ =>/ _)" 10)
    1.93 +  ""            :: case_syn => cases_syn            ("_")
    1.94 +  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ | _")
    1.95  
    1.96  translations
    1.97    "x ~= y"      == "~ (x = y)"