--- 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)"
--- 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
--- 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)})"
--- 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)"
--- 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})"
--- 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]"
--- 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"
--- 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))"
--- 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)"
--- 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)"
--- 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"
--- 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"
--- 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]