removed quotes from types in consts and syntax sections
authorclasohm
Wed Nov 29 16:44:59 1995 +0100 (1995-11-29)
changeset 13707361ac9b024d
parent 1369 b82815e61b30
child 1371 2f97fc253763
removed quotes from types in consts and syntax sections
src/HOL/Arith.thy
src/HOL/Finite.thy
src/HOL/Gfp.thy
src/HOL/HOL.thy
src/HOL/Lfp.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Ord.thy
src/HOL/Prod.thy
src/HOL/Set.thy
src/HOL/Sexp.thy
src/HOL/Sum.thy
src/HOL/Univ.thy
     1.1 --- a/src/HOL/Arith.thy	Mon Nov 27 13:44:56 1995 +0100
     1.2 +++ b/src/HOL/Arith.thy	Wed Nov 29 16:44:59 1995 +0100
     1.3 @@ -12,8 +12,8 @@
     1.4    nat :: {plus, minus, times}
     1.5  
     1.6  consts
     1.7 -  pred      :: "nat => nat"
     1.8 -  div, mod  :: "[nat, nat] => nat"  (infixl 70)
     1.9 +  pred      :: nat => nat
    1.10 +  div, mod  :: [nat, nat] => nat  (infixl 70)
    1.11  
    1.12  defs
    1.13    pred_def  "pred(m) == nat_rec m 0 (%n r.n)"
     2.1 --- a/src/HOL/Finite.thy	Mon Nov 27 13:44:56 1995 +0100
     2.2 +++ b/src/HOL/Finite.thy	Wed Nov 29 16:44:59 1995 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  *)
     2.5  
     2.6  Finite = Lfp +
     2.7 -consts Fin :: "'a set => 'a set set"
     2.8 +consts Fin :: 'a set => 'a set set
     2.9  
    2.10  inductive "Fin(A)"
    2.11    intrs
     3.1 --- a/src/HOL/Gfp.thy	Mon Nov 27 13:44:56 1995 +0100
     3.2 +++ b/src/HOL/Gfp.thy	Wed Nov 29 16:44:59 1995 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  *)
     3.5  
     3.6  Gfp = Lfp +
     3.7 -consts gfp :: "['a set=>'a set] => 'a set"
     3.8 +consts gfp :: ['a set=>'a set] => 'a set
     3.9  defs
    3.10   (*greatest fixed point*)
    3.11   gfp_def "gfp(f) == Union({u. u <= f(u)})"
     4.1 --- a/src/HOL/HOL.thy	Mon Nov 27 13:44:56 1995 +0100
     4.2 +++ b/src/HOL/HOL.thy	Wed Nov 29 16:44:59 1995 +0100
     4.3 @@ -35,33 +35,33 @@
     4.4  
     4.5    (* Constants *)
     4.6  
     4.7 -  Trueprop      :: "bool => prop"                     ("(_)" 5)
     4.8 -  not           :: "bool => bool"                     ("~ _" [40] 40)
     4.9 -  True, False   :: "bool"
    4.10 -  If            :: "[bool, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
    4.11 -  Inv           :: "('a => 'b) => ('b => 'a)"
    4.12 +  Trueprop      :: bool => prop                     ("(_)" 5)
    4.13 +  not           :: bool => bool                     ("~ _" [40] 40)
    4.14 +  True, False   :: bool
    4.15 +  If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    4.16 +  Inv           :: ('a => 'b) => ('b => 'a)
    4.17  
    4.18    (* Binders *)
    4.19  
    4.20 -  Eps           :: "('a => bool) => 'a"
    4.21 -  All           :: "('a => bool) => bool"             (binder "! " 10)
    4.22 -  Ex            :: "('a => bool) => bool"             (binder "? " 10)
    4.23 -  Ex1           :: "('a => bool) => bool"             (binder "?! " 10)
    4.24 -  Let           :: "['a, 'a => 'b] => 'b"
    4.25 +  Eps           :: ('a => bool) => 'a
    4.26 +  All           :: ('a => bool) => bool             (binder "! " 10)
    4.27 +  Ex            :: ('a => bool) => bool             (binder "? " 10)
    4.28 +  Ex1           :: ('a => bool) => bool             (binder "?! " 10)
    4.29 +  Let           :: ['a, 'a => 'b] => 'b
    4.30  
    4.31    (* Infixes *)
    4.32  
    4.33 -  o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl 55)
    4.34 -  "="           :: "['a, 'a] => bool"                 (infixl 50)
    4.35 -  "&"           :: "[bool, bool] => bool"             (infixr 35)
    4.36 -  "|"           :: "[bool, bool] => bool"             (infixr 30)
    4.37 -  "-->"         :: "[bool, bool] => bool"             (infixr 25)
    4.38 +  o             :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    4.39 +  "="           :: ['a, 'a] => bool                 (infixl 50)
    4.40 +  "&"           :: [bool, bool] => bool             (infixr 35)
    4.41 +  "|"           :: [bool, bool] => bool             (infixr 30)
    4.42 +  "-->"         :: [bool, bool] => bool             (infixr 25)
    4.43  
    4.44    (* Overloaded Constants *)
    4.45  
    4.46 -  "+"           :: "['a::plus, 'a] => 'a"             (infixl 65)
    4.47 -  "-"           :: "['a::minus, 'a] => 'a"            (infixl 65)
    4.48 -  "*"           :: "['a::times, 'a] => 'a"            (infixl 70)
    4.49 +  "+"           :: ['a::plus, 'a] => 'a             (infixl 65)
    4.50 +  "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
    4.51 +  "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    4.52  
    4.53  
    4.54  types
    4.55 @@ -70,29 +70,29 @@
    4.56  
    4.57  syntax
    4.58  
    4.59 -  "~="          :: "['a, 'a] => bool"                 (infixl 50)
    4.60 +  "~="          :: ['a, 'a] => bool                 (infixl 50)
    4.61  
    4.62 -  "@Eps"        :: "[pttrn,bool] => 'a"               ("(3@ _./ _)" 10)
    4.63 +  "@Eps"        :: [pttrn,bool] => 'a               ("(3@ _./ _)" 10)
    4.64  
    4.65    (* Alternative Quantifiers *)
    4.66  
    4.67 -  "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
    4.68 -  "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)
    4.69 -  "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" 10)
    4.70 +  "*All"        :: [idts, bool] => bool             ("(3ALL _./ _)" 10)
    4.71 +  "*Ex"         :: [idts, bool] => bool             ("(3EX _./ _)" 10)
    4.72 +  "*Ex1"        :: [idts, bool] => bool             ("(3EX! _./ _)" 10)
    4.73  
    4.74    (* Let expressions *)
    4.75  
    4.76 -  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
    4.77 -  ""            :: "letbind => letbinds"              ("_")
    4.78 -  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
    4.79 -  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
    4.80 +  "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
    4.81 +  ""            :: letbind => letbinds              ("_")
    4.82 +  "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
    4.83 +  "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
    4.84  
    4.85    (* Case expressions *)
    4.86  
    4.87 -  "@case"       :: "['a, cases_syn] => 'b"            ("(case _ of/ _)" 10)
    4.88 -  "@case1"      :: "['a, 'b] => case_syn"             ("(2_ =>/ _)" 10)
    4.89 -  ""            :: "case_syn => cases_syn"            ("_")
    4.90 -  "@case2"      :: "[case_syn, cases_syn] => cases_syn"   ("_/ | _")
    4.91 +  "@case"       :: ['a, cases_syn] => 'b            ("(case _ of/ _)" 10)
    4.92 +  "@case1"      :: ['a, 'b] => case_syn             ("(2_ =>/ _)" 10)
    4.93 +  ""            :: case_syn => cases_syn            ("_")
    4.94 +  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ | _")
    4.95  
    4.96  translations
    4.97    "x ~= y"      == "~ (x = y)"
     5.1 --- a/src/HOL/Lfp.thy	Mon Nov 27 13:44:56 1995 +0100
     5.2 +++ b/src/HOL/Lfp.thy	Wed Nov 29 16:44:59 1995 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  *)
     5.5  
     5.6  Lfp = mono + Prod +
     5.7 -consts lfp :: "['a set=>'a set] => 'a set"
     5.8 +consts lfp :: ['a set=>'a set] => 'a set
     5.9  defs
    5.10   (*least fixed point*)
    5.11   lfp_def "lfp(f) == Inter({u. f(u) <= u})"
     6.1 --- a/src/HOL/List.thy	Mon Nov 27 13:44:56 1995 +0100
     6.2 +++ b/src/HOL/List.thy	Wed Nov 29 16:44:59 1995 +0100
     6.3 @@ -13,28 +13,28 @@
     6.4  
     6.5  consts
     6.6  
     6.7 -  "@"	    :: "['a list, 'a list] => 'a list"		(infixr 65)
     6.8 -  drop      :: "[nat, 'a list] => 'a list"
     6.9 -  filter    :: "['a => bool, 'a list] => 'a list"
    6.10 -  flat      :: "'a list list => 'a list"
    6.11 -  foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
    6.12 -  hd        :: "'a list => 'a"
    6.13 -  length    :: "'a list => nat"
    6.14 -  list_all  :: "('a => bool) => ('a list => bool)"
    6.15 -  map       :: "('a=>'b) => ('a list => 'b list)"
    6.16 -  mem       :: "['a, 'a list] => bool"			(infixl 55)
    6.17 -  nth       :: "[nat, 'a list] => 'a"
    6.18 -  take      :: "[nat, 'a list] => 'a list"
    6.19 -  tl,ttl    :: "'a list => 'a list"
    6.20 -  rev       :: "'a list => 'a list"
    6.21 +  "@"	    :: ['a list, 'a list] => 'a list		(infixr 65)
    6.22 +  drop      :: [nat, 'a list] => 'a list
    6.23 +  filter    :: ['a => bool, 'a list] => 'a list
    6.24 +  flat      :: 'a list list => 'a list
    6.25 +  foldl     :: [['b,'a] => 'b, 'b, 'a list] => 'b
    6.26 +  hd        :: 'a list => 'a
    6.27 +  length    :: 'a list => nat
    6.28 +  list_all  :: ('a => bool) => ('a list => bool)
    6.29 +  map       :: ('a=>'b) => ('a list => 'b list)
    6.30 +  mem       :: ['a, 'a list] => bool			(infixl 55)
    6.31 +  nth       :: [nat, 'a list] => 'a
    6.32 +  take      :: [nat, 'a list] => 'a list
    6.33 +  tl,ttl    :: 'a list => 'a list
    6.34 +  rev       :: 'a list => 'a list
    6.35  
    6.36  syntax
    6.37    (* list Enumeration *)
    6.38 -  "@list"   :: "args => 'a list"                        ("[(_)]")
    6.39 +  "@list"   :: args => 'a list                        ("[(_)]")
    6.40  
    6.41    (* Special syntax for list_all and filter *)
    6.42 -  "@Alls"	:: "[idt, 'a list, bool] => bool"	("(2Alls _:_./ _)" 10)
    6.43 -  "@filter"	:: "[idt, 'a list, bool] => 'a list"	("(1[_:_ ./ _])")
    6.44 +  "@Alls"	:: [idt, 'a list, bool] => bool	("(2Alls _:_./ _)" 10)
    6.45 +  "@filter"	:: [idt, 'a list, bool] => 'a list	("(1[_:_ ./ _])")
    6.46  
    6.47  translations
    6.48    "[x, xs]"     == "x#[xs]"
     7.1 --- a/src/HOL/Nat.thy	Mon Nov 27 13:44:56 1995 +0100
     7.2 +++ b/src/HOL/Nat.thy	Wed Nov 29 16:44:59 1995 +0100
     7.3 @@ -19,8 +19,8 @@
     7.4    ind :: term
     7.5  
     7.6  consts
     7.7 -  Zero_Rep      :: "ind"
     7.8 -  Suc_Rep       :: "ind => ind"
     7.9 +  Zero_Rep      :: ind
    7.10 +  Suc_Rep       :: ind => ind
    7.11  
    7.12  rules
    7.13    (*the axiom of infinity in 2 parts*)
    7.14 @@ -43,11 +43,11 @@
    7.15  (* abstract constants and syntax *)
    7.16  
    7.17  consts
    7.18 -  "0"           :: "nat"                ("0")
    7.19 -  Suc           :: "nat => nat"
    7.20 -  nat_case      :: "['a, nat => 'a, nat] => 'a"
    7.21 +  "0"           :: nat                ("0")
    7.22 +  Suc           :: nat => nat
    7.23 +  nat_case      :: ['a, nat => 'a, nat] => 'a
    7.24    pred_nat      :: "(nat * nat) set"
    7.25 -  nat_rec       :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
    7.26 +  nat_rec       :: [nat, 'a, [nat, 'a] => 'a] => 'a
    7.27  
    7.28  translations
    7.29    "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
     8.1 --- a/src/HOL/Ord.thy	Mon Nov 27 13:44:56 1995 +0100
     8.2 +++ b/src/HOL/Ord.thy	Wed Nov 29 16:44:59 1995 +0100
     8.3 @@ -12,9 +12,9 @@
     8.4    ord < term
     8.5  
     8.6  consts
     8.7 -  "<", "<="     :: "['a::ord, 'a] => bool"              (infixl 50)
     8.8 -  mono          :: "['a::ord => 'b::ord] => bool"       (*monotonicity*)
     8.9 -  min, max      :: "['a::ord, 'a] => 'a"
    8.10 +  "<", "<="     :: ['a::ord, 'a] => bool              (infixl 50)
    8.11 +  mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
    8.12 +  min, max      :: ['a::ord, 'a] => 'a
    8.13  
    8.14  defs
    8.15    mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
     9.1 --- a/src/HOL/Prod.thy	Mon Nov 27 13:44:56 1995 +0100
     9.2 +++ b/src/HOL/Prod.thy	Wed Nov 29 16:44:59 1995 +0100
     9.3 @@ -14,7 +14,7 @@
     9.4  (* type definition *)
     9.5  
     9.6  consts
     9.7 -  Pair_Rep      :: "['a, 'b] => ['a, 'b] => bool"
     9.8 +  Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
     9.9  
    9.10  defs
    9.11    Pair_Rep_def  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    9.12 @@ -40,9 +40,9 @@
    9.13  syntax
    9.14    "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
    9.15  
    9.16 -  "@pttrn"  :: "[pttrn,pttrns] => pttrn"              ("'(_,/_')")
    9.17 -  ""        :: " pttrn         => pttrns"             ("_")
    9.18 -  "@pttrns" :: "[pttrn,pttrns] => pttrns"             ("_,/_")
    9.19 +  "@pttrn"  :: [pttrn,pttrns] => pttrn              ("'(_,/_')")
    9.20 +  ""        ::  pttrn         => pttrns             ("_")
    9.21 +  "@pttrns" :: [pttrn,pttrns] => pttrns             ("_,/_")
    9.22  
    9.23  translations
    9.24    "(x, y, z)"   == "(x, (y, z))"
    9.25 @@ -69,7 +69,7 @@
    9.26    unit = "{p. p = True}"
    9.27  
    9.28  consts
    9.29 -  "()"          :: "unit"                           ("'(')")
    9.30 +  "()"          :: unit                           ("'(')")
    9.31  
    9.32  defs
    9.33    Unity_def     "() == Abs_Unit(True)"
    10.1 --- a/src/HOL/Set.thy	Mon Nov 27 13:44:56 1995 +0100
    10.2 +++ b/src/HOL/Set.thy	Wed Nov 29 16:44:59 1995 +0100
    10.3 @@ -16,45 +16,45 @@
    10.4    set :: (term) {ord, minus}
    10.5  
    10.6  consts
    10.7 -  "{}"          :: "'a set"                           ("{}")
    10.8 -  insert        :: "['a, 'a set] => 'a set"
    10.9 -  Collect       :: "('a => bool) => 'a set"               (*comprehension*)
   10.10 -  Compl         :: "('a set) => 'a set"                   (*complement*)
   10.11 -  Int           :: "['a set, 'a set] => 'a set"       (infixl 70)
   10.12 -  Un            :: "['a set, 'a set] => 'a set"       (infixl 65)
   10.13 -  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"     (*general*)
   10.14 -  UNION1        :: "['a => 'b set] => 'b set"         (binder "UN " 10)
   10.15 -  INTER1        :: "['a => 'b set] => 'b set"         (binder "INT " 10)
   10.16 -  Union, Inter  :: "(('a set)set) => 'a set"              (*of a set*)
   10.17 -  Pow           :: "'a set => 'a set set"                 (*powerset*)
   10.18 -  range         :: "('a => 'b) => 'b set"                 (*of function*)
   10.19 -  Ball, Bex     :: "['a set, 'a => bool] => bool"         (*bounded quantifiers*)
   10.20 -  inj, surj     :: "('a => 'b) => bool"                   (*inj/surjective*)
   10.21 -  inj_onto      :: "['a => 'b, 'a set] => bool"
   10.22 -  "``"          :: "['a => 'b, 'a set] => ('b set)"   (infixl 90)
   10.23 -  ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
   10.24 +  "{}"          :: 'a set                           ("{}")
   10.25 +  insert        :: ['a, 'a set] => 'a set
   10.26 +  Collect       :: ('a => bool) => 'a set               (*comprehension*)
   10.27 +  Compl         :: ('a set) => 'a set                   (*complement*)
   10.28 +  Int           :: ['a set, 'a set] => 'a set       (infixl 70)
   10.29 +  Un            :: ['a set, 'a set] => 'a set       (infixl 65)
   10.30 +  UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
   10.31 +  UNION1        :: ['a => 'b set] => 'b set         (binder "UN " 10)
   10.32 +  INTER1        :: ['a => 'b set] => 'b set         (binder "INT " 10)
   10.33 +  Union, Inter  :: (('a set)set) => 'a set              (*of a set*)
   10.34 +  Pow           :: 'a set => 'a set set                 (*powerset*)
   10.35 +  range         :: ('a => 'b) => 'b set                 (*of function*)
   10.36 +  Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
   10.37 +  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
   10.38 +  inj_onto      :: ['a => 'b, 'a set] => bool
   10.39 +  "``"          :: ['a => 'b, 'a set] => ('b set)   (infixl 90)
   10.40 +  ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)
   10.41  
   10.42  
   10.43  syntax
   10.44  
   10.45 -  "~:"          :: "['a, 'a set] => bool"             (infixl 50)
   10.46 +  "~:"          :: ['a, 'a set] => bool             (infixl 50)
   10.47  
   10.48 -  "@Finset"     :: "args => 'a set"                   ("{(_)}")
   10.49 +  "@Finset"     :: args => 'a set                   ("{(_)}")
   10.50  
   10.51 -  "@Coll"       :: "[pttrn, bool] => 'a set"          ("(1{_./ _})")
   10.52 -  "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
   10.53 +  "@Coll"       :: [pttrn, bool] => 'a set          ("(1{_./ _})")
   10.54 +  "@SetCompr"   :: ['a, idts, bool] => 'a set       ("(1{_ |/_./ _})")
   10.55  
   10.56    (* Big Intersection / Union *)
   10.57  
   10.58 -  "@INTER"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
   10.59 -  "@UNION"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
   10.60 +  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
   10.61 +  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
   10.62  
   10.63    (* Bounded Quantifiers *)
   10.64  
   10.65 -  "@Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
   10.66 -  "@Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
   10.67 -  "*Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
   10.68 -  "*Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
   10.69 +  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" 10)
   10.70 +  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" 10)
   10.71 +  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" 10)
   10.72 +  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" 10)
   10.73  
   10.74  translations
   10.75    "x ~: y"      == "~ (x : y)"
    11.1 --- a/src/HOL/Sexp.thy	Mon Nov 27 13:44:56 1995 +0100
    11.2 +++ b/src/HOL/Sexp.thy	Wed Nov 29 16:44:59 1995 +0100
    11.3 @@ -8,7 +8,7 @@
    11.4  
    11.5  Sexp = Univ +
    11.6  consts
    11.7 -  sexp      :: "'a item set"
    11.8 +  sexp      :: 'a item set
    11.9  
   11.10    sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
   11.11                  'a item] => 'b"
    12.1 --- a/src/HOL/Sum.thy	Mon Nov 27 13:44:56 1995 +0100
    12.2 +++ b/src/HOL/Sum.thy	Wed Nov 29 16:44:59 1995 +0100
    12.3 @@ -11,8 +11,8 @@
    12.4  (* type definition *)
    12.5  
    12.6  consts
    12.7 -  Inl_Rep       :: "['a, 'a, 'b, bool] => bool"
    12.8 -  Inr_Rep       :: "['b, 'a, 'b, bool] => bool"
    12.9 +  Inl_Rep       :: ['a, 'a, 'b, bool] => bool
   12.10 +  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
   12.11  
   12.12  defs
   12.13    Inl_Rep_def   "Inl_Rep == (%a. %x y p. x=a & p)"
   12.14 @@ -32,7 +32,7 @@
   12.15  
   12.16    (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
   12.17    "plus"        :: "['a set, 'b set] => ('a + 'b) set"        (infixr 65)
   12.18 -  Part          :: "['a set, 'b => 'a] => 'a set"
   12.19 +  Part          :: ['a set, 'b => 'a] => 'a set
   12.20  
   12.21  translations
   12.22    "case p of Inl(x) => a | Inr(y) => b" == "sum_case (%x.a) (%y.b) p"
    13.1 --- a/src/HOL/Univ.thy	Mon Nov 27 13:44:56 1995 +0100
    13.2 +++ b/src/HOL/Univ.thy	Wed Nov 29 16:44:59 1995 +0100
    13.3 @@ -22,27 +22,27 @@
    13.4    'a item = "'a node set"
    13.5  
    13.6  consts
    13.7 -  Least     :: "(nat=>bool) => nat"    (binder "LEAST " 10)
    13.8 +  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    13.9  
   13.10    apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
   13.11 -  Push      :: "[nat, nat=>nat] => (nat=>nat)"
   13.12 +  Push      :: [nat, nat=>nat] => (nat=>nat)
   13.13  
   13.14 -  Push_Node :: "[nat, 'a node] => 'a node"
   13.15 -  ndepth    :: "'a node => nat"
   13.16 +  Push_Node :: [nat, 'a node] => 'a node
   13.17 +  ndepth    :: 'a node => nat
   13.18  
   13.19    Atom      :: "('a+nat) => 'a item"
   13.20 -  Leaf      :: "'a => 'a item"
   13.21 -  Numb      :: "nat => 'a item"
   13.22 -  "$"       :: "['a item, 'a item]=> 'a item"   (infixr 60)
   13.23 -  In0,In1   :: "'a item => 'a item"
   13.24 +  Leaf      :: 'a => 'a item
   13.25 +  Numb      :: nat => 'a item
   13.26 +  "$"       :: ['a item, 'a item]=> 'a item   (infixr 60)
   13.27 +  In0,In1   :: 'a item => 'a item
   13.28  
   13.29 -  ntrunc    :: "[nat, 'a item] => 'a item"
   13.30 +  ntrunc    :: [nat, 'a item] => 'a item
   13.31  
   13.32 -  "<*>"  :: "['a item set, 'a item set]=> 'a item set" (infixr 80)
   13.33 -  "<+>"  :: "['a item set, 'a item set]=> 'a item set" (infixr 70)
   13.34 +  "<*>"  :: ['a item set, 'a item set]=> 'a item set (infixr 80)
   13.35 +  "<+>"  :: ['a item set, 'a item set]=> 'a item set (infixr 70)
   13.36  
   13.37 -  Split  :: "[['a item, 'a item]=>'b, 'a item] => 'b"
   13.38 -  Case   :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
   13.39 +  Split  :: [['a item, 'a item]=>'b, 'a item] => 'b
   13.40 +  Case   :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b
   13.41  
   13.42    diag   :: "'a set => ('a * 'a)set"
   13.43    "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set]