# HG changeset patch # User clasohm # Date 817659899 -3600 # Node ID 7361ac9b024d6d1bf2545b2fc5a3ee152c6319a4 # Parent b82815e61b30d7104d57ab6abd1ba29c9b05c8ad removed quotes from types in consts and syntax sections diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Arith.thy --- a/src/HOL/Arith.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Arith.thy Wed Nov 29 16:44:59 1995 +0100 @@ -12,8 +12,8 @@ nat :: {plus, minus, times} consts - pred :: "nat => nat" - div, mod :: "[nat, nat] => nat" (infixl 70) + pred :: nat => nat + div, mod :: [nat, nat] => nat (infixl 70) defs pred_def "pred(m) == nat_rec m 0 (%n r.n)" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Finite.thy --- a/src/HOL/Finite.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Finite.thy Wed Nov 29 16:44:59 1995 +0100 @@ -7,7 +7,7 @@ *) Finite = Lfp + -consts Fin :: "'a set => 'a set set" +consts Fin :: 'a set => 'a set set inductive "Fin(A)" intrs diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Gfp.thy --- a/src/HOL/Gfp.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Gfp.thy Wed Nov 29 16:44:59 1995 +0100 @@ -7,7 +7,7 @@ *) Gfp = Lfp + -consts gfp :: "['a set=>'a set] => 'a set" +consts gfp :: ['a set=>'a set] => 'a set defs (*greatest fixed point*) gfp_def "gfp(f) == Union({u. u <= f(u)})" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/HOL.thy Wed Nov 29 16:44:59 1995 +0100 @@ -35,33 +35,33 @@ (* Constants *) - Trueprop :: "bool => prop" ("(_)" 5) - not :: "bool => bool" ("~ _" [40] 40) - True, False :: "bool" - If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) - Inv :: "('a => 'b) => ('b => 'a)" + Trueprop :: bool => prop ("(_)" 5) + not :: bool => bool ("~ _" [40] 40) + True, False :: bool + If :: [bool, 'a, 'a] => 'a ("(if (_)/ then (_)/ else (_))" 10) + Inv :: ('a => 'b) => ('b => 'a) (* Binders *) - Eps :: "('a => bool) => 'a" - All :: "('a => bool) => bool" (binder "! " 10) - Ex :: "('a => bool) => bool" (binder "? " 10) - Ex1 :: "('a => bool) => bool" (binder "?! " 10) - Let :: "['a, 'a => 'b] => 'b" + Eps :: ('a => bool) => 'a + All :: ('a => bool) => bool (binder "! " 10) + Ex :: ('a => bool) => bool (binder "? " 10) + Ex1 :: ('a => bool) => bool (binder "?! " 10) + Let :: ['a, 'a => 'b] => 'b (* Infixes *) - o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl 55) - "=" :: "['a, 'a] => bool" (infixl 50) - "&" :: "[bool, bool] => bool" (infixr 35) - "|" :: "[bool, bool] => bool" (infixr 30) - "-->" :: "[bool, bool] => bool" (infixr 25) + o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) + "=" :: ['a, 'a] => bool (infixl 50) + "&" :: [bool, bool] => bool (infixr 35) + "|" :: [bool, bool] => bool (infixr 30) + "-->" :: [bool, bool] => bool (infixr 25) (* Overloaded Constants *) - "+" :: "['a::plus, 'a] => 'a" (infixl 65) - "-" :: "['a::minus, 'a] => 'a" (infixl 65) - "*" :: "['a::times, 'a] => 'a" (infixl 70) + "+" :: ['a::plus, 'a] => 'a (infixl 65) + "-" :: ['a::minus, 'a] => 'a (infixl 65) + "*" :: ['a::times, 'a] => 'a (infixl 70) types @@ -70,29 +70,29 @@ syntax - "~=" :: "['a, 'a] => bool" (infixl 50) + "~=" :: ['a, 'a] => bool (infixl 50) - "@Eps" :: "[pttrn,bool] => 'a" ("(3@ _./ _)" 10) + "@Eps" :: [pttrn,bool] => 'a ("(3@ _./ _)" 10) (* Alternative Quantifiers *) - "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) - "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) - "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) + "*All" :: [idts, bool] => bool ("(3ALL _./ _)" 10) + "*Ex" :: [idts, bool] => bool ("(3EX _./ _)" 10) + "*Ex1" :: [idts, bool] => bool ("(3EX! _./ _)" 10) (* Let expressions *) - "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) - "" :: "letbind => letbinds" ("_") - "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") - "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) + "_bind" :: [pttrn, 'a] => letbind ("(2_ =/ _)" 10) + "" :: letbind => letbinds ("_") + "_binds" :: [letbind, letbinds] => letbinds ("_;/ _") + "_Let" :: [letbinds, 'a] => 'a ("(let (_)/ in (_))" 10) (* Case expressions *) - "@case" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) - "@case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) - "" :: "case_syn => cases_syn" ("_") - "@case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") + "@case" :: ['a, cases_syn] => 'b ("(case _ of/ _)" 10) + "@case1" :: ['a, 'b] => case_syn ("(2_ =>/ _)" 10) + "" :: case_syn => cases_syn ("_") + "@case2" :: [case_syn, cases_syn] => cases_syn ("_/ | _") translations "x ~= y" == "~ (x = y)" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Lfp.thy --- a/src/HOL/Lfp.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Lfp.thy Wed Nov 29 16:44:59 1995 +0100 @@ -7,7 +7,7 @@ *) Lfp = mono + Prod + -consts lfp :: "['a set=>'a set] => 'a set" +consts lfp :: ['a set=>'a set] => 'a set defs (*least fixed point*) lfp_def "lfp(f) == Inter({u. f(u) <= u})" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/List.thy --- a/src/HOL/List.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/List.thy Wed Nov 29 16:44:59 1995 +0100 @@ -13,28 +13,28 @@ consts - "@" :: "['a list, 'a list] => 'a list" (infixr 65) - drop :: "[nat, 'a list] => 'a list" - filter :: "['a => bool, 'a list] => 'a list" - flat :: "'a list list => 'a list" - foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b" - hd :: "'a list => 'a" - length :: "'a list => nat" - list_all :: "('a => bool) => ('a list => bool)" - map :: "('a=>'b) => ('a list => 'b list)" - mem :: "['a, 'a list] => bool" (infixl 55) - nth :: "[nat, 'a list] => 'a" - take :: "[nat, 'a list] => 'a list" - tl,ttl :: "'a list => 'a list" - rev :: "'a list => 'a list" + "@" :: ['a list, 'a list] => 'a list (infixr 65) + drop :: [nat, 'a list] => 'a list + filter :: ['a => bool, 'a list] => 'a list + flat :: 'a list list => 'a list + foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b + hd :: 'a list => 'a + length :: 'a list => nat + list_all :: ('a => bool) => ('a list => bool) + map :: ('a=>'b) => ('a list => 'b list) + mem :: ['a, 'a list] => bool (infixl 55) + nth :: [nat, 'a list] => 'a + take :: [nat, 'a list] => 'a list + tl,ttl :: 'a list => 'a list + rev :: 'a list => 'a list syntax (* list Enumeration *) - "@list" :: "args => 'a list" ("[(_)]") + "@list" :: args => 'a list ("[(_)]") (* Special syntax for list_all and filter *) - "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10) - "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])") + "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10) + "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])") translations "[x, xs]" == "x#[xs]" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Nat.thy Wed Nov 29 16:44:59 1995 +0100 @@ -19,8 +19,8 @@ ind :: term consts - Zero_Rep :: "ind" - Suc_Rep :: "ind => ind" + Zero_Rep :: ind + Suc_Rep :: ind => ind rules (*the axiom of infinity in 2 parts*) @@ -43,11 +43,11 @@ (* abstract constants and syntax *) consts - "0" :: "nat" ("0") - Suc :: "nat => nat" - nat_case :: "['a, nat => 'a, nat] => 'a" + "0" :: nat ("0") + Suc :: nat => nat + nat_case :: ['a, nat => 'a, nat] => 'a pred_nat :: "(nat * nat) set" - nat_rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" + nat_rec :: [nat, 'a, [nat, 'a] => 'a] => 'a translations "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Ord.thy --- a/src/HOL/Ord.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Ord.thy Wed Nov 29 16:44:59 1995 +0100 @@ -12,9 +12,9 @@ ord < term consts - "<", "<=" :: "['a::ord, 'a] => bool" (infixl 50) - mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) - min, max :: "['a::ord, 'a] => 'a" + "<", "<=" :: ['a::ord, 'a] => bool (infixl 50) + mono :: ['a::ord => 'b::ord] => bool (*monotonicity*) + min, max :: ['a::ord, 'a] => 'a defs mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Prod.thy --- a/src/HOL/Prod.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Prod.thy Wed Nov 29 16:44:59 1995 +0100 @@ -14,7 +14,7 @@ (* type definition *) consts - Pair_Rep :: "['a, 'b] => ['a, 'b] => bool" + Pair_Rep :: ['a, 'b] => ['a, 'b] => bool defs Pair_Rep_def "Pair_Rep == (%a b. %x y. x=a & y=b)" @@ -40,9 +40,9 @@ syntax "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") - "@pttrn" :: "[pttrn,pttrns] => pttrn" ("'(_,/_')") - "" :: " pttrn => pttrns" ("_") - "@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_") + "@pttrn" :: [pttrn,pttrns] => pttrn ("'(_,/_')") + "" :: pttrn => pttrns ("_") + "@pttrns" :: [pttrn,pttrns] => pttrns ("_,/_") translations "(x, y, z)" == "(x, (y, z))" @@ -69,7 +69,7 @@ unit = "{p. p = True}" consts - "()" :: "unit" ("'(')") + "()" :: unit ("'(')") defs Unity_def "() == Abs_Unit(True)" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Set.thy --- a/src/HOL/Set.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Set.thy Wed Nov 29 16:44:59 1995 +0100 @@ -16,45 +16,45 @@ set :: (term) {ord, minus} consts - "{}" :: "'a set" ("{}") - insert :: "['a, 'a set] => 'a set" - Collect :: "('a => bool) => 'a set" (*comprehension*) - Compl :: "('a set) => 'a set" (*complement*) - Int :: "['a set, 'a set] => 'a set" (infixl 70) - Un :: "['a set, 'a set] => 'a set" (infixl 65) - UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) - UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10) - INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10) - Union, Inter :: "(('a set)set) => 'a set" (*of a set*) - Pow :: "'a set => 'a set set" (*powerset*) - range :: "('a => 'b) => 'b set" (*of function*) - Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*) - inj, surj :: "('a => 'b) => bool" (*inj/surjective*) - inj_onto :: "['a => 'b, 'a set] => bool" - "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90) - ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*) + "{}" :: 'a set ("{}") + insert :: ['a, 'a set] => 'a set + Collect :: ('a => bool) => 'a set (*comprehension*) + Compl :: ('a set) => 'a set (*complement*) + Int :: ['a set, 'a set] => 'a set (infixl 70) + Un :: ['a set, 'a set] => 'a set (infixl 65) + UNION, INTER :: ['a set, 'a => 'b set] => 'b set (*general*) + UNION1 :: ['a => 'b set] => 'b set (binder "UN " 10) + INTER1 :: ['a => 'b set] => 'b set (binder "INT " 10) + Union, Inter :: (('a set)set) => 'a set (*of a set*) + Pow :: 'a set => 'a set set (*powerset*) + range :: ('a => 'b) => 'b set (*of function*) + Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) + inj, surj :: ('a => 'b) => bool (*inj/surjective*) + inj_onto :: ['a => 'b, 'a set] => bool + "``" :: ['a => 'b, 'a set] => ('b set) (infixl 90) + ":" :: ['a, 'a set] => bool (infixl 50) (*membership*) syntax - "~:" :: "['a, 'a set] => bool" (infixl 50) + "~:" :: ['a, 'a set] => bool (infixl 50) - "@Finset" :: "args => 'a set" ("{(_)}") + "@Finset" :: args => 'a set ("{(_)}") - "@Coll" :: "[pttrn, bool] => 'a set" ("(1{_./ _})") - "@SetCompr" :: "['a, idts, bool] => 'a set" ("(1{_ |/_./ _})") + "@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})") + "@SetCompr" :: ['a, idts, bool] => 'a set ("(1{_ |/_./ _})") (* Big Intersection / Union *) - "@INTER" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10) - "@UNION" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10) + "@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3INT _:_./ _)" 10) + "@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3UN _:_./ _)" 10) (* Bounded Quantifiers *) - "@Ball" :: "[pttrn, 'a set, bool] => bool" ("(3! _:_./ _)" 10) - "@Bex" :: "[pttrn, 'a set, bool] => bool" ("(3? _:_./ _)" 10) - "*Ball" :: "[pttrn, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) - "*Bex" :: "[pttrn, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) + "@Ball" :: [pttrn, 'a set, bool] => bool ("(3! _:_./ _)" 10) + "@Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" 10) + "*Ball" :: [pttrn, 'a set, bool] => bool ("(3ALL _:_./ _)" 10) + "*Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" 10) translations "x ~: y" == "~ (x : y)" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Sexp.thy --- a/src/HOL/Sexp.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Sexp.thy Wed Nov 29 16:44:59 1995 +0100 @@ -8,7 +8,7 @@ Sexp = Univ + consts - sexp :: "'a item set" + sexp :: 'a item set sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 'a item] => 'b" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Sum.thy --- a/src/HOL/Sum.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Sum.thy Wed Nov 29 16:44:59 1995 +0100 @@ -11,8 +11,8 @@ (* type definition *) consts - Inl_Rep :: "['a, 'a, 'b, bool] => bool" - Inr_Rep :: "['b, 'a, 'b, bool] => bool" + Inl_Rep :: ['a, 'a, 'b, bool] => bool + Inr_Rep :: ['b, 'a, 'b, bool] => bool defs Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)" @@ -32,7 +32,7 @@ (*disjoint sum for sets; the operator + is overloaded with wrong type!*) "plus" :: "['a set, 'b set] => ('a + 'b) set" (infixr 65) - Part :: "['a set, 'b => 'a] => 'a set" + Part :: ['a set, 'b => 'a] => 'a set translations "case p of Inl(x) => a | Inr(y) => b" == "sum_case (%x.a) (%y.b) p" diff -r b82815e61b30 -r 7361ac9b024d src/HOL/Univ.thy --- a/src/HOL/Univ.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Univ.thy Wed Nov 29 16:44:59 1995 +0100 @@ -22,27 +22,27 @@ 'a item = "'a node set" consts - Least :: "(nat=>bool) => nat" (binder "LEAST " 10) + Least :: (nat=>bool) => nat (binder "LEAST " 10) apfst :: "['a=>'c, 'a*'b] => 'c*'b" - Push :: "[nat, nat=>nat] => (nat=>nat)" + Push :: [nat, nat=>nat] => (nat=>nat) - Push_Node :: "[nat, 'a node] => 'a node" - ndepth :: "'a node => nat" + Push_Node :: [nat, 'a node] => 'a node + ndepth :: 'a node => nat Atom :: "('a+nat) => 'a item" - Leaf :: "'a => 'a item" - Numb :: "nat => 'a item" - "$" :: "['a item, 'a item]=> 'a item" (infixr 60) - In0,In1 :: "'a item => 'a item" + Leaf :: 'a => 'a item + Numb :: nat => 'a item + "$" :: ['a item, 'a item]=> 'a item (infixr 60) + In0,In1 :: 'a item => 'a item - ntrunc :: "[nat, 'a item] => 'a item" + ntrunc :: [nat, 'a item] => 'a item - "<*>" :: "['a item set, 'a item set]=> 'a item set" (infixr 80) - "<+>" :: "['a item set, 'a item set]=> 'a item set" (infixr 70) + "<*>" :: ['a item set, 'a item set]=> 'a item set (infixr 80) + "<+>" :: ['a item set, 'a item set]=> 'a item set (infixr 70) - Split :: "[['a item, 'a item]=>'b, 'a item] => 'b" - Case :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b" + Split :: [['a item, 'a item]=>'b, 'a item] => 'b + Case :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b diag :: "'a set => ('a * 'a)set" "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set]