--- a/src/ZF/AC/AC16_WO4.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/AC16_WO4.thy Sat Dec 09 13:36:11 1995 +0100
@@ -7,11 +7,11 @@
consts
- ww :: "[i, i] => i"
- s_u :: "[i, i, i, i] => i"
- MM :: "[i, i, i] => i"
- LL :: "[i, i, i] => i"
- GG :: "[i, i, i] => i"
+ ww :: [i, i] => i
+ s_u :: [i, i, i, i] => i
+ MM :: [i, i, i] => i
+ LL :: [i, i, i] => i
+ GG :: [i, i, i] => i
defs
--- a/src/ZF/AC/AC18_AC19.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/AC18_AC19.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
AC18_AC19 = AC_Equiv +
consts
- u_ :: "i => i"
+ u_ :: i => i
defs
--- a/src/ZF/AC/AC_Equiv.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/AC_Equiv.thy Sat Dec 09 13:36:11 1995 +0100
@@ -17,19 +17,19 @@
consts
(* Well Ordering Theorems *)
- WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: "o"
- WO4 :: "i => o"
+ WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: o
+ WO4 :: i => o
(* Axioms of Choice *)
AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9,
- AC11, AC12, AC14, AC15, AC17, AC19 :: "o"
- AC10, AC13 :: "i => o"
- AC16 :: "[i, i] => o"
- AC18 :: "prop" ("AC18")
+ AC11, AC12, AC14, AC15, AC17, AC19 :: o
+ AC10, AC13 :: i => o
+ AC16 :: [i, i] => o
+ AC18 :: prop ("AC18")
(* Auxiliary definitions used in definitions *)
- pairwise_disjoint :: "i => o"
- sets_of_size_between :: "[i, i, i] => o"
+ pairwise_disjoint :: i => o
+ sets_of_size_between :: [i, i, i] => o
defs
--- a/src/ZF/AC/DC.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/DC.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,9 +9,9 @@
consts
- DC :: "i => o"
- DC0 :: "o"
- ff :: "[i, i, i, i] => i"
+ DC :: i => o
+ DC0 :: o
+ ff :: [i, i, i, i] => i
rules
--- a/src/ZF/AC/HH.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/HH.thy Sat Dec 09 13:36:11 1995 +0100
@@ -12,7 +12,7 @@
consts
- HH :: "[i, i, i] => i"
+ HH :: [i, i, i] => i
defs
--- a/src/ZF/AC/Hartog.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/Hartog.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
consts
- Hartog :: "i => i"
+ Hartog :: i => i
defs
--- a/src/ZF/AC/OrdQuant.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/OrdQuant.thy Sat Dec 09 13:36:11 1995 +0100
@@ -10,16 +10,16 @@
consts
(* Ordinal Quantifiers *)
- oall, oex :: "[i, i => o] => o"
+ oall, oex :: [i, i => o] => o
(* Ordinal Union *)
- OUnion :: "[i, i => i] => i"
+ OUnion :: [i, i => i] => i
syntax
- "@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10)
- "@oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10)
- "@OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10)
+ "@oall" :: [idt, i, o] => o ("(3ALL _<_./ _)" 10)
+ "@oex" :: [idt, i, o] => o ("(3EX _<_./ _)" 10)
+ "@OUNION" :: [idt, i, i] => i ("(3UN _<_./ _)" 10)
translations
--- a/src/ZF/AC/Transrec2.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/Transrec2.thy Sat Dec 09 13:36:11 1995 +0100
@@ -10,7 +10,7 @@
consts
- transrec2 :: "[i, i, [i,i]=>i] =>i"
+ transrec2 :: [i, i, [i,i]=>i] =>i
defs
--- a/src/ZF/AC/WO6_WO1.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Sat Dec 09 13:36:11 1995 +0100
@@ -12,10 +12,10 @@
consts
(* Auxiliary definitions used in proof *)
- NN :: "i => i"
- uu :: "[i, i, i, i] => i"
- vv1, ww1, gg1 :: "[i, i, i] => i"
- vv2, ww2, gg2 :: "[i, i, i, i] => i"
+ NN :: i => i
+ uu :: [i, i, i, i] => i
+ vv1, ww1, gg1 :: [i, i, i] => i
+ vv2, ww2, gg2 :: [i, i, i, i] => i
defs
--- a/src/ZF/AC/first.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/first.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
consts
- first :: "[i, i, i] => o"
+ first :: [i, i, i] => o
defs
--- a/src/ZF/AC/recfunAC16.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/recfunAC16.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
consts
- recfunAC16 :: "[i, i, i, i] => i"
+ recfunAC16 :: [i, i, i, i] => i
defs
--- a/src/ZF/Arith.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Arith.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,12 +8,12 @@
Arith = Epsilon + "simpdata" +
consts
- rec :: "[i, i, [i,i]=>i]=>i"
- "#*" :: "[i,i]=>i" (infixl 70)
- div :: "[i,i]=>i" (infixl 70)
- mod :: "[i,i]=>i" (infixl 70)
- "#+" :: "[i,i]=>i" (infixl 65)
- "#-" :: "[i,i]=>i" (infixl 65)
+ rec :: [i, i, [i,i]=>i]=>i
+ "#*" :: [i,i]=>i (infixl 70)
+ div :: [i,i]=>i (infixl 70)
+ mod :: [i,i]=>i (infixl 70)
+ "#+" :: [i,i]=>i (infixl 65)
+ "#-" :: [i,i]=>i (infixl 65)
defs
rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
--- a/src/ZF/Bool.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Bool.thy Sat Dec 09 13:36:11 1995 +0100
@@ -10,14 +10,14 @@
Bool = ZF + "simpdata" +
consts
- "1" :: "i" ("1")
- "2" :: "i" ("2")
- bool :: "i"
- cond :: "[i,i,i]=>i"
- not :: "i=>i"
- "and" :: "[i,i]=>i" (infixl 70)
- or :: "[i,i]=>i" (infixl 65)
- xor :: "[i,i]=>i" (infixl 65)
+ "1" :: i ("1")
+ "2" :: i ("2")
+ bool :: i
+ cond :: [i,i,i]=>i
+ not :: i=>i
+ "and" :: [i,i]=>i (infixl 70)
+ or :: [i,i]=>i (infixl 65)
+ xor :: [i,i]=>i (infixl 65)
translations
"1" == "succ(0)"
--- a/src/ZF/Cardinal.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Cardinal.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,11 +8,11 @@
Cardinal = OrderType + Fixedpt + Nat + Sum +
consts
- Least :: "(i=>o) => i" (binder "LEAST " 10)
+ Least :: (i=>o) => i (binder "LEAST " 10)
eqpoll, lepoll,
- lesspoll :: "[i,i] => o" (infixl 50)
- cardinal :: "i=>i" ("|_|")
- Finite, Card :: "i=>o"
+ lesspoll :: [i,i] => o (infixl 50)
+ cardinal :: i=>i ("|_|")
+ Finite, Card :: i=>o
defs
--- a/src/ZF/CardinalArith.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/CardinalArith.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,12 +9,12 @@
CardinalArith = Cardinal + OrderArith + Arith + Finite +
consts
- InfCard :: "i=>o"
- "|*|" :: "[i,i]=>i" (infixl 70)
- "|+|" :: "[i,i]=>i" (infixl 65)
- csquare_rel :: "i=>i"
- jump_cardinal :: "i=>i"
- csucc :: "i=>i"
+ InfCard :: i=>o
+ "|*|" :: [i,i]=>i (infixl 70)
+ "|+|" :: [i,i]=>i (infixl 65)
+ csquare_rel :: i=>i
+ jump_cardinal :: i=>i
+ csucc :: i=>i
defs
--- a/src/ZF/Coind/BCR.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/BCR.thy Sat Dec 09 13:36:11 1995 +0100
@@ -10,14 +10,14 @@
parameter of the proof. A concrete version could be defined inductively.*)
consts
- isof :: "[i,i] => o"
+ isof :: [i,i] => o
rules
isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
(*Its extension to environments*)
consts
- isofenv :: "[i,i] => o"
+ isofenv :: [i,i] => o
defs
isofenv_def "isofenv(ve,te) ==
ve_dom(ve) = te_dom(te) &
--- a/src/ZF/Coind/Dynamic.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Dynamic.thy Sat Dec 09 13:36:11 1995 +0100
@@ -7,7 +7,7 @@
Dynamic = Values +
consts
- EvalRel :: "i"
+ EvalRel :: i
inductive
domains "EvalRel" <= "ValEnv * Exp * Val"
intrs
--- a/src/ZF/Coind/ECR.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/ECR.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
(* The extended correspondence relation *)
consts
- HasTyRel :: "i"
+ HasTyRel :: i
coinductive
domains "HasTyRel" <= "Val * Ty"
intrs
@@ -28,7 +28,7 @@
(* Pointwise extension to environments *)
consts
- hastyenv :: "[i,i] => o"
+ hastyenv :: [i,i] => o
defs
hastyenv_def
" hastyenv(ve,te) ==
--- a/src/ZF/Coind/Language.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Language.thy Sat Dec 09 13:36:11 1995 +0100
@@ -7,8 +7,8 @@
Language ="Datatype" + QUniv +
consts
- Const :: "i" (* Abstract type of constants *)
- c_app :: "[i,i] => i" (*Abstract constructor for fun application*)
+ Const :: i (* Abstract type of constants *)
+ c_app :: [i,i] => i (*Abstract constructor for fun application*)
rules
constNEE "c:Const ==> c ~= 0"
@@ -16,8 +16,8 @@
consts
- Exp :: "i" (* Datatype of expressions *)
- ExVar :: "i" (* Abstract type of variables *)
+ Exp :: i (* Datatype of expressions *)
+ ExVar :: i (* Abstract type of variables *)
datatype <= "univ(Const Un ExVar)"
"Exp" = e_const("c:Const")
| e_var("x:ExVar")
--- a/src/ZF/Coind/Map.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Map.thy Sat Dec 09 13:36:11 1995 +0100
@@ -7,8 +7,8 @@
Map = QUniv +
consts
- TMap :: "[i,i] => i"
- PMap :: "[i,i] => i"
+ TMap :: [i,i] => i
+ PMap :: [i,i] => i
defs
TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
@@ -16,9 +16,9 @@
(* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
consts
- map_emp :: "i"
- map_owr :: "[i,i,i]=>i"
- map_app :: "[i,i]=>i"
+ map_emp :: i
+ map_owr :: [i,i,i]=>i
+ map_app :: [i,i]=>i
defs
map_emp_def "map_emp == 0"
map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
--- a/src/ZF/Coind/Static.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Static.thy Sat Dec 09 13:36:11 1995 +0100
@@ -7,7 +7,7 @@
Static = BCR +
consts
- ElabRel :: "i"
+ ElabRel :: i
inductive
domains "ElabRel" <= "TyEnv * Exp * Ty"
intrs
--- a/src/ZF/Coind/Types.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Types.thy Sat Dec 09 13:36:11 1995 +0100
@@ -7,8 +7,8 @@
Types = Language +
consts
- Ty :: "i" (* Datatype of types *)
- TyConst :: "i" (* Abstract type of type constants *)
+ Ty :: i (* Datatype of types *)
+ TyConst :: i (* Abstract type of type constants *)
datatype <= "univ(TyConst)"
"Ty" = t_const("tc:TyConst")
| t_fun("t1:Ty","t2:Ty")
@@ -17,21 +17,21 @@
(* Definition of type environments and associated operators *)
consts
- TyEnv :: "i"
+ TyEnv :: i
datatype <= "univ(Ty Un ExVar)"
"TyEnv" = te_emp
| te_owr("te:TyEnv","x:ExVar","t:Ty")
consts
- te_rec :: "[i,i,[i,i,i,i]=>i] => i"
+ te_rec :: [i,i,[i,i,i,i]=>i] => i
defs
te_rec_def
"te_rec(te,c,h) ==
Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
consts
- te_dom :: "i => i"
- te_app :: "[i,i] => i"
+ te_dom :: i => i
+ te_app :: [i,i] => i
defs
te_dom_def "te_dom(te) == te_rec(te,0,% te x t r.r Un {x})"
te_app_def "te_app(te,x) == te_rec(te,0, % te y t r.if(x=y,t,r))"
--- a/src/ZF/Coind/Values.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Values.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
(* Values, values environments and associated operators *)
consts
- Val, ValEnv, Val_ValEnv :: "i"
+ Val, ValEnv, Val_ValEnv :: i
codatatype <= "quniv(Const Un ExVar Un Exp)"
"Val" = v_const("c:Const")
| v_clos("x:ExVar","e:Exp","ve:ValEnv")
@@ -19,10 +19,10 @@
type_intrs "[A_into_univ, mapQU]"
consts
- ve_emp :: "i"
- ve_owr :: "[i,i,i] => i"
- ve_dom :: "i=>i"
- ve_app :: "[i,i] => i"
+ ve_emp :: i
+ ve_owr :: [i,i,i] => i
+ ve_dom :: i=>i
+ ve_app :: [i,i] => i
defs
ve_emp_def "ve_emp == ve_mk(map_emp)"
ve_owr_def
--- a/src/ZF/Epsilon.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Epsilon.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
Epsilon = Nat + "mono" +
consts
- eclose,rank :: "i=>i"
- transrec :: "[i, [i,i]=>i] =>i"
+ eclose,rank :: i=>i
+ transrec :: [i, [i,i]=>i] =>i
defs
eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
--- a/src/ZF/EquivClass.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/EquivClass.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
EquivClass = Rel + Perm +
consts
- "'/" :: "[i,i]=>i" (infixl 90) (*set of equiv classes*)
- congruent :: "[i,i=>i]=>o"
- congruent2 :: "[i,[i,i]=>i]=>o"
+ "'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*)
+ congruent :: [i,i=>i]=>o
+ congruent2 :: [i,[i,i]=>i]=>o
defs
quotient_def "A/r == {r``{x} . x:A}"
--- a/src/ZF/Finite.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Finite.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
Finite = Arith + Inductive +
consts
- Fin :: "i=>i"
- FiniteFun :: "[i,i]=>i" ("(_ -||>/ _)" [61, 60] 60)
+ Fin :: i=>i
+ FiniteFun :: [i,i]=>i ("(_ -||>/ _)" [61, 60] 60)
inductive
domains "Fin(A)" <= "Pow(A)"
--- a/src/ZF/Fixedpt.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Fixedpt.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
Fixedpt = ZF + "domrange" +
consts
- bnd_mono :: "[i,i=>i]=>o"
- lfp, gfp :: "[i,i=>i]=>i"
+ bnd_mono :: [i,i=>i]=>o
+ lfp, gfp :: [i,i=>i]=>i
defs
(*monotone operator from Pow(D) to itself*)
--- a/src/ZF/IMP/Com.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/IMP/Com.thy Sat Dec 09 13:36:11 1995 +0100
@@ -11,8 +11,8 @@
Com = Datatype +
(** Arithmetic expressions **)
-consts loc :: "i"
- aexp :: "i"
+consts loc :: i
+ aexp :: i
datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
"aexp" = N ("n: nat")
@@ -22,8 +22,8 @@
(** Evaluation of arithmetic expressions **)
-consts evala :: "i"
- "@evala" :: "[i,i,i] => o" ("<_,_>/ -a-> _" [0,0,50] 50)
+consts evala :: i
+ "@evala" :: [i,i,i] => o ("<_,_>/ -a-> _" [0,0,50] 50)
translations
"<ae,sig> -a-> n" == "<ae,sig,n> : evala"
inductive
@@ -39,7 +39,7 @@
(** Boolean expressions **)
-consts bexp :: "i"
+consts bexp :: i
datatype <= "univ(aexp Un ((nat*nat)->bool) )"
"bexp" = true
@@ -51,8 +51,8 @@
(** Evaluation of boolean expressions **)
-consts evalb :: "i"
- "@evalb" :: "[i,i,i] => o" ("<_,_>/ -b-> _" [0,0,50] 50)
+consts evalb :: i
+ "@evalb" :: [i,i,i] => o ("<_,_>/ -b-> _" [0,0,50] 50)
translations
"<be,sig> -b-> b" == "<be,sig,b> : evalb"
@@ -76,7 +76,7 @@
(** Commands **)
-consts com :: "i"
+consts com :: i
datatype <= "univ(loc Un aexp Un bexp)"
"com" = skip
@@ -89,9 +89,9 @@
with [| m: nat; x: loc; ... |] ==> ... It usually will need parentheses.*)
(** Execution of commands **)
-consts evalc :: "i"
- "@evalc" :: "[i,i,i] => o" ("<_,_>/ -c-> _" [0,0,50] 50)
- "assign" :: "[i,i,i] => i" ("_[_'/_]" [95,0,0] 95)
+consts evalc :: i
+ "@evalc" :: [i,i,i] => o ("<_,_>/ -c-> _" [0,0,50] 50)
+ "assign" :: [i,i,i] => i ("_[_'/_]" [95,0,0] 95)
translations
"<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
--- a/src/ZF/IMP/Denotation.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/IMP/Denotation.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,10 +9,10 @@
Denotation = Com +
consts
- A :: "i => i => i"
- B :: "i => i => i"
- C :: "i => i"
- Gamma :: "[i,i,i] => i"
+ A :: i => i => i
+ B :: i => i => i
+ C :: i => i
+ Gamma :: [i,i,i] => i
rules (*NOT definitional*)
A_nat_def "A(N(n)) == (%sigma. n)"
--- a/src/ZF/Let.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Let.thy Sat Dec 09 13:36:11 1995 +0100
@@ -12,13 +12,13 @@
letbinds letbind
consts
- Let :: "['a, 'a => 'b] => 'b"
+ Let :: ['a, 'a => 'b] => 'b
syntax
- "_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)
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
--- a/src/ZF/List.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/List.thy Sat Dec 09 13:36:11 1995 +0100
@@ -13,20 +13,20 @@
List = Datatype +
consts
- "@" :: "[i,i]=>i" (infixr 60)
- list_rec :: "[i, i, [i,i,i]=>i] => i"
- map :: "[i=>i, i] => i"
- length,rev :: "i=>i"
- flat :: "i=>i"
- list_add :: "i=>i"
- hd,tl :: "i=>i"
- drop :: "[i,i]=>i"
+ "@" :: [i,i]=>i (infixr 60)
+ list_rec :: [i, i, [i,i,i]=>i] => i
+ map :: [i=>i, i] => i
+ length,rev :: i=>i
+ flat :: i=>i
+ list_add :: i=>i
+ hd,tl :: i=>i
+ drop :: [i,i]=>i
(* List Enumeration *)
- "[]" :: "i" ("[]")
- "@List" :: "is => i" ("[(_)]")
+ "[]" :: i ("[]")
+ "@List" :: is => i ("[(_)]")
- list :: "i=>i"
+ list :: i=>i
datatype
--- a/src/ZF/Nat.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Nat.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
Nat = Ordinal + Bool + "mono" +
consts
- nat :: "i"
- nat_case :: "[i, i=>i, i]=>i"
- nat_rec :: "[i, i, [i,i]=>i]=>i"
+ nat :: i
+ nat_case :: [i, i=>i, i]=>i
+ nat_rec :: [i, i, [i,i]=>i]=>i
defs
--- a/src/ZF/Order.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Order.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,13 +8,13 @@
Order = WF + Perm +
consts
- part_ord :: "[i,i]=>o" (*Strict partial ordering*)
- linear, tot_ord :: "[i,i]=>o" (*Strict total ordering*)
- well_ord :: "[i,i]=>o" (*Well-ordering*)
- mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*)
- ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*)
- pred :: "[i,i,i]=>i" (*Set of predecessors*)
- ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*)
+ part_ord :: [i,i]=>o (*Strict partial ordering*)
+ linear, tot_ord :: [i,i]=>o (*Strict total ordering*)
+ well_ord :: [i,i]=>o (*Well-ordering*)
+ mono_map :: [i,i,i,i]=>i (*Order-preserving maps*)
+ ord_iso :: [i,i,i,i]=>i (*Order isomorphisms*)
+ pred :: [i,i,i]=>i (*Set of predecessors*)
+ ord_iso_map :: [i,i,i,i]=>i (*Construction for linearity theorem*)
defs
part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
--- a/src/ZF/OrderArith.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/OrderArith.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
OrderArith = Order + Sum +
consts
- radd, rmult :: "[i,i,i,i]=>i"
- rvimage :: "[i,i,i]=>i"
+ radd, rmult :: [i,i,i,i]=>i
+ rvimage :: [i,i,i]=>i
defs
(*disjoint sum of two relations; underlies ordinal addition*)
--- a/src/ZF/OrderType.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/OrderType.thy Sat Dec 09 13:36:11 1995 +0100
@@ -10,14 +10,14 @@
OrderType = OrderArith + Ordinal +
consts
- ordermap :: "[i,i]=>i"
- ordertype :: "[i,i]=>i"
+ ordermap :: [i,i]=>i
+ ordertype :: [i,i]=>i
- Ord_alt :: "i => o"
+ Ord_alt :: i => o
- "**" :: "[i,i]=>i" (infixl 70)
- "++" :: "[i,i]=>i" (infixl 65)
- "--" :: "[i,i]=>i" (infixl 65)
+ "**" :: [i,i]=>i (infixl 70)
+ "++" :: [i,i]=>i (infixl 65)
+ "--" :: [i,i]=>i (infixl 65)
defs
--- a/src/ZF/Ordinal.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Ordinal.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,11 +8,11 @@
Ordinal = WF + Bool + "simpdata" + "equalities" +
consts
- Memrel :: "i=>i"
- Transset,Ord :: "i=>o"
- "<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*)
- "le" :: "[i,i] => o" (infixl 50) (*less than or equals*)
- Limit :: "i=>o"
+ Memrel :: i=>i
+ Transset,Ord :: i=>o
+ "<" :: [i,i] => o (infixl 50) (*less than on ordinals*)
+ "le" :: [i,i] => o (infixl 50) (*less than or equals*)
+ Limit :: i=>o
translations
"x le y" == "x < succ(y)"
--- a/src/ZF/Perm.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Perm.thy Sat Dec 09 13:36:11 1995 +0100
@@ -11,9 +11,9 @@
Perm = ZF + "mono" +
consts
- O :: "[i,i]=>i" (infixr 60)
- id :: "i=>i"
- inj,surj,bij:: "[i,i]=>i"
+ O :: [i,i]=>i (infixr 60)
+ id :: i=>i
+ inj,surj,bij:: [i,i]=>i
defs
--- a/src/ZF/QPair.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/QPair.thy Sat Dec 09 13:36:11 1995 +0100
@@ -13,19 +13,19 @@
QPair = Sum + "simpdata" +
consts
- QPair :: "[i, i] => i" ("<(_;/ _)>")
- qfst,qsnd :: "i => i"
- qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*)
- qconverse :: "i => i"
- QSigma :: "[i, i => i] => i"
+ QPair :: [i, i] => i ("<(_;/ _)>")
+ qfst,qsnd :: i => i
+ qsplit :: [[i, i] => 'a, i] => 'a::logic (*for pattern-matching*)
+ qconverse :: i => i
+ QSigma :: [i, i => i] => i
- "<+>" :: "[i,i]=>i" (infixr 65)
- QInl,QInr :: "i=>i"
- qcase :: "[i=>i, i=>i, i]=>i"
+ "<+>" :: [i,i]=>i (infixr 65)
+ QInl,QInr :: i=>i
+ qcase :: [i=>i, i=>i, i]=>i
syntax
- "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
- "<*>" :: "[i, i] => i" (infixr 80)
+ "@QSUM" :: [idt, i, i] => i ("(3QSUM _:_./ _)" 10)
+ "<*>" :: [i, i] => i (infixr 80)
translations
"QSUM x:A. B" => "QSigma(A, %x. B)"
--- a/src/ZF/QUniv.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/QUniv.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,7 +8,7 @@
QUniv = Univ + QPair + "mono" + "equalities" +
consts
- quniv :: "i=>i"
+ quniv :: i=>i
defs
quniv_def "quniv(A) == Pow(univ(eclose(A)))"
--- a/src/ZF/Rel.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Rel.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
Rel = ZF +
consts
- refl,irrefl,equiv :: "[i,i]=>o"
- sym,asym,antisym,trans :: "i=>o"
- trans_on :: "[i,i]=>o" ("trans[_]'(_')")
+ refl,irrefl,equiv :: [i,i]=>o
+ sym,asym,antisym,trans :: i=>o
+ trans_on :: [i,i]=>o ("trans[_]'(_')")
defs
refl_def "refl(A,r) == (ALL x: A. <x,x> : r)"
--- a/src/ZF/Resid/Confluence.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Confluence.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
Confluence = Reduction+
consts
- confluence :: "i=>o"
- strip :: "o"
+ confluence :: i=>o
+ strip :: o
defs
confluence_def "confluence(R) ==
--- a/src/ZF/Resid/Conversion.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Conversion.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,10 +9,10 @@
Conversion = Confluence+
consts
- Sconv1 :: "i"
- "<-1->" :: "[i,i]=>o" (infixl 50)
- Sconv :: "i"
- "<--->" :: "[i,i]=>o" (infixl 50)
+ Sconv1 :: i
+ "<-1->" :: [i,i]=>o (infixl 50)
+ Sconv :: i
+ "<--->" :: [i,i]=>o (infixl 50)
translations
"a<-1->b" == "<a,b>:Sconv1"
--- a/src/ZF/Resid/Redex.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Redex.thy Sat Dec 09 13:36:11 1995 +0100
@@ -7,7 +7,7 @@
Redex = Univ +
consts
- redexes :: "i"
+ redexes :: i
datatype
"redexes" = Var ("n: nat")
@@ -17,7 +17,7 @@
consts
- redex_rec :: "[i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i"
+ redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
defs
redex_rec_def
--- a/src/ZF/Resid/Reduction.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Reduction.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
Reduction = Terms+
consts
- Sred1, Sred, Spar_red1,Spar_red :: "i"
- "-1->","--->","=1=>", "===>" :: "[i,i]=>o" (infixl 50)
+ Sred1, Sred, Spar_red1,Spar_red :: i
+ "-1->","--->","=1=>", "===>" :: [i,i]=>o (infixl 50)
translations
"a -1-> b" == "<a,b>:Sred1"
--- a/src/ZF/Resid/Residuals.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Residuals.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,9 +9,9 @@
Residuals = Substitution+
consts
- Sres :: "i"
- residuals :: "[i,i,i]=>i"
- "|>" :: "[i,i]=>i" (infixl 70)
+ Sres :: i
+ residuals :: [i,i,i]=>i
+ "|>" :: [i,i]=>i (infixl 70)
translations
"residuals(u,v,w)" == "<u,v,w>:Sres"
--- a/src/ZF/Resid/SubUnion.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/SubUnion.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,10 +8,10 @@
SubUnion = Redex +
consts
- Ssub,Scomp,Sreg :: "i"
- "<==","~" :: "[i,i]=>o" (infixl 70)
- un :: "[i,i]=>i" (infixl 70)
- regular :: "i=>o"
+ Ssub,Scomp,Sreg :: i
+ "<==","~" :: [i,i]=>o (infixl 70)
+ un :: [i,i]=>i (infixl 70)
+ regular :: i=>o
translations
"a<==b" == "<a,b>:Ssub"
--- a/src/ZF/Resid/Substitution.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Substitution.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,10 +8,10 @@
Substitution = SubUnion +
consts
- lift_rec :: "[i,i]=> i"
- lift :: "i=>i"
- subst_rec :: "[i,i,i]=> i"
- "'/" :: "[i,i]=>i" (infixl 70) (*subst*)
+ lift_rec :: [i,i]=> i
+ lift :: i=>i
+ subst_rec :: [i,i,i]=> i
+ "'/" :: [i,i]=>i (infixl 70) (*subst*)
translations
"lift(r)" == "lift_rec(r,0)"
"u/v" == "subst_rec(u,v,0)"
--- a/src/ZF/Resid/Terms.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Terms.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
Terms = Cube+
consts
- lambda :: "i"
- unmark :: "i=>i"
- Apl :: "[i,i]=>i"
+ lambda :: i
+ unmark :: i=>i
+ Apl :: [i,i]=>i
translations
"Apl(n,m)" == "App(0,n,m)"
--- a/src/ZF/Sum.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Sum.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,10 +9,10 @@
Sum = Bool + "simpdata" +
consts
- "+" :: "[i,i]=>i" (infixr 65)
- Inl,Inr :: "i=>i"
- case :: "[i=>i, i=>i, i]=>i"
- Part :: "[i,i=>i] => i"
+ "+" :: [i,i]=>i (infixr 65)
+ Inl,Inr :: i=>i
+ case :: [i=>i, i=>i, i]=>i
+ Part :: [i,i=>i] => i
defs
sum_def "A+B == {0}*A Un {1}*B"
--- a/src/ZF/Trancl.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Trancl.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
Trancl = Fixedpt + Perm + "mono" + Rel +
consts
- rtrancl :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*)
- trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
+ rtrancl :: i=>i ("(_^*)" [100] 100) (*refl/transitive closure*)
+ trancl :: i=>i ("(_^+)" [100] 100) (*transitive closure*)
defs
rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
--- a/src/ZF/Univ.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Univ.thy Sat Dec 09 13:36:11 1995 +0100
@@ -13,10 +13,10 @@
Univ = Arith + Sum + Finite + "mono" +
consts
- Vfrom :: "[i,i]=>i"
- Vset :: "i=>i"
- Vrec :: "[i, [i,i]=>i] =>i"
- univ :: "i=>i"
+ Vfrom :: [i,i]=>i
+ Vset :: i=>i
+ Vrec :: [i, [i,i]=>i] =>i
+ univ :: i=>i
translations
"Vset(x)" == "Vfrom(0,x)"
--- a/src/ZF/WF.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/WF.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,13 +8,13 @@
WF = Trancl + "mono" + "equalities" +
consts
- wf :: "i=>o"
- wf_on :: "[i,i]=>o" ("wf[_]'(_')")
+ wf :: i=>o
+ wf_on :: [i,i]=>o ("wf[_]'(_')")
- wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"
- wfrec_on :: "[i, i, i, [i,i]=>i] =>i" ("wfrec[_]'(_,_,_')")
- is_recfun :: "[i, i, [i,i]=>i, i] =>o"
- the_recfun :: "[i, i, [i,i]=>i] =>i"
+ wftrec,wfrec :: [i, i, [i,i]=>i] =>i
+ wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')")
+ is_recfun :: [i, i, [i,i]=>i, i] =>o
+ the_recfun :: [i, i, [i,i]=>i] =>i
defs
(*r is a well-founded relation*)
--- a/src/ZF/ZF.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ZF.thy Sat Dec 09 13:36:11 1995 +0100
@@ -16,68 +16,68 @@
consts
- "0" :: "i" ("0") (*the empty set*)
- Pow :: "i => i" (*power sets*)
- Inf :: "i" (*infinite set*)
+ "0" :: i ("0") (*the empty set*)
+ Pow :: i => i (*power sets*)
+ Inf :: i (*infinite set*)
(* Bounded Quantifiers *)
- Ball, Bex :: "[i, i => o] => o"
+ Ball, Bex :: [i, i => o] => o
(* General Union and Intersection *)
- Union,Inter :: "i => i"
+ Union,Inter :: i => i
(* Variations on Replacement *)
- PrimReplace :: "[i, [i, i] => o] => i"
- Replace :: "[i, [i, i] => o] => i"
- RepFun :: "[i, i => i] => i"
- Collect :: "[i, i => o] => i"
+ PrimReplace :: [i, [i, i] => o] => i
+ Replace :: [i, [i, i] => o] => i
+ RepFun :: [i, i => i] => i
+ Collect :: [i, i => o] => i
(* Descriptions *)
- The :: "(i => o) => i" (binder "THE " 10)
- if :: "[o, i, i] => i"
+ The :: (i => o) => i (binder "THE " 10)
+ if :: [o, i, i] => i
(* Finite Sets *)
- Upair, cons :: "[i, i] => i"
- succ :: "i => i"
+ Upair, cons :: [i, i] => i
+ succ :: i => i
(* Ordered Pairing *)
- Pair :: "[i, i] => i"
- fst, snd :: "i => i"
- split :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*)
+ Pair :: [i, i] => i
+ fst, snd :: i => i
+ split :: [[i, i] => 'a, i] => 'a::logic (*for pattern-matching*)
(* Sigma and Pi Operators *)
- Sigma, Pi :: "[i, i => i] => i"
+ Sigma, Pi :: [i, i => i] => i
(* Relations and Functions *)
- domain :: "i => i"
- range :: "i => i"
- field :: "i => i"
- converse :: "i => i"
- function :: "i => o" (*is a relation a function?*)
- Lambda :: "[i, i => i] => i"
- restrict :: "[i, i] => i"
+ domain :: i => i
+ range :: i => i
+ field :: i => i
+ converse :: i => i
+ function :: i => o (*is a relation a function?*)
+ Lambda :: [i, i => i] => i
+ restrict :: [i, i] => i
(* Infixes in order of decreasing precedence *)
- "``" :: "[i, i] => i" (infixl 90) (*image*)
- "-``" :: "[i, i] => i" (infixl 90) (*inverse image*)
- "`" :: "[i, i] => i" (infixl 90) (*function application*)
-(*"*" :: "[i, i] => i" (infixr 80) (*Cartesian product*)*)
- "Int" :: "[i, i] => i" (infixl 70) (*binary intersection*)
- "Un" :: "[i, i] => i" (infixl 65) (*binary union*)
- "-" :: "[i, i] => i" (infixl 65) (*set difference*)
-(*"->" :: "[i, i] => i" (infixr 60) (*function space*)*)
- "<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
- ":" :: "[i, i] => o" (infixl 50) (*membership relation*)
-(*"~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)*)
+ "``" :: [i, i] => i (infixl 90) (*image*)
+ "-``" :: [i, i] => i (infixl 90) (*inverse image*)
+ "`" :: [i, i] => i (infixl 90) (*function application*)
+(*"*" :: [i, i] => i (infixr 80) (*Cartesian product*)*)
+ "Int" :: [i, i] => i (infixl 70) (*binary intersection*)
+ "Un" :: [i, i] => i (infixl 65) (*binary union*)
+ "-" :: [i, i] => i (infixl 65) (*set difference*)
+(*"->" :: [i, i] => i (infixr 60) (*function space*)*)
+ "<=" :: [i, i] => o (infixl 50) (*subset relation*)
+ ":" :: [i, i] => o (infixl 50) (*membership relation*)
+(*"~:" :: [i, i] => o (infixl 50) (*negated membership relation*)*)
types
@@ -85,29 +85,29 @@
pttrns
syntax
- "" :: "i => is" ("_")
- "@Enum" :: "[i, is] => is" ("_,/ _")
- "~:" :: "[i, i] => o" (infixl 50)
- "@Finset" :: "is => i" ("{(_)}")
- "@Tuple" :: "[i, is] => i" ("<(_,/ _)>")
- "@Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})")
- "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
- "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51])
- "@INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10)
- "@UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10)
- "@PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10)
- "@SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10)
- "->" :: "[i, i] => i" (infixr 60)
- "*" :: "[i, i] => i" (infixr 80)
- "@lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10)
- "@Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10)
- "@Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10)
+ "" :: i => is ("_")
+ "@Enum" :: [i, is] => is ("_,/ _")
+ "~:" :: [i, i] => o (infixl 50)
+ "@Finset" :: is => i ("{(_)}")
+ "@Tuple" :: [i, is] => i ("<(_,/ _)>")
+ "@Collect" :: [pttrn, i, o] => i ("(1{_: _ ./ _})")
+ "@Replace" :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _: _, _})")
+ "@RepFun" :: [i, pttrn, i] => i ("(1{_ ./ _: _})" [51,0,51])
+ "@INTER" :: [pttrn, i, i] => i ("(3INT _:_./ _)" 10)
+ "@UNION" :: [pttrn, i, i] => i ("(3UN _:_./ _)" 10)
+ "@PROD" :: [pttrn, i, i] => i ("(3PROD _:_./ _)" 10)
+ "@SUM" :: [pttrn, i, i] => i ("(3SUM _:_./ _)" 10)
+ "->" :: [i, i] => i (infixr 60)
+ "*" :: [i, i] => i (infixr 80)
+ "@lam" :: [pttrn, i, i] => i ("(3lam _:_./ _)" 10)
+ "@Ball" :: [pttrn, i, o] => o ("(3ALL _:_./ _)" 10)
+ "@Bex" :: [pttrn, i, o] => o ("(3EX _:_./ _)" 10)
(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
- "@pttrn" :: "pttrns => pttrn" ("<_>")
- "" :: " pttrn => pttrns" ("_")
- "@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_")
+ "@pttrn" :: pttrns => pttrn ("<_>")
+ "" :: pttrn => pttrns ("_")
+ "@pttrns" :: [pttrn,pttrns] => pttrns ("_,/_")
translations
"x ~: y" == "~ (x : y)"
--- a/src/ZF/Zorn.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Zorn.thy Sat Dec 09 13:36:11 1995 +0100
@@ -14,10 +14,10 @@
Zorn = OrderArith + AC + Inductive +
consts
- Subset_rel :: "i=>i"
- increasing :: "i=>i"
- chain, maxchain :: "i=>i"
- super :: "[i,i]=>i"
+ Subset_rel :: i=>i
+ increasing :: i=>i
+ chain, maxchain :: i=>i
+ super :: [i,i]=>i
defs
Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
@@ -34,7 +34,7 @@
are therefore unconditional.
**)
consts
- "TFin" :: "[i,i]=>i"
+ "TFin" :: [i,i]=>i
inductive
domains "TFin(S,next)" <= "Pow(S)"
--- a/src/ZF/ex/Acc.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Acc.thy Sat Dec 09 13:36:11 1995 +0100
@@ -12,7 +12,7 @@
Acc = WF + Inductive +
consts
- acc :: "i=>i"
+ acc :: i=>i
inductive
domains "acc(r)" <= "field(r)"
--- a/src/ZF/ex/BT.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/BT.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,12 +8,12 @@
BT = Datatype +
consts
- bt_rec :: "[i, i, [i,i,i,i,i]=>i] => i"
- n_nodes :: "i=>i"
- n_leaves :: "i=>i"
- bt_reflect :: "i=>i"
+ bt_rec :: [i, i, [i,i,i,i,i]=>i] => i
+ n_nodes :: i=>i
+ n_leaves :: i=>i
+ bt_reflect :: i=>i
- bt :: "i=>i"
+ bt :: i=>i
datatype
"bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)")
--- a/src/ZF/ex/Bin.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Bin.thy Sat Dec 09 13:36:11 1995 +0100
@@ -21,18 +21,18 @@
Bin = Integ + Datatype + "twos_compl" +
consts
- bin_rec :: "[i, i, i, [i,i,i]=>i] => i"
- integ_of_bin :: "i=>i"
- norm_Bcons :: "[i,i]=>i"
- bin_succ :: "i=>i"
- bin_pred :: "i=>i"
- bin_minus :: "i=>i"
- bin_add,bin_mult :: "[i,i]=>i"
+ bin_rec :: [i, i, i, [i,i,i]=>i] => i
+ integ_of_bin :: i=>i
+ norm_Bcons :: [i,i]=>i
+ bin_succ :: i=>i
+ bin_pred :: i=>i
+ bin_minus :: i=>i
+ bin_add,bin_mult :: [i,i]=>i
- bin :: "i"
+ bin :: i
syntax
- "_Int" :: "xnum => i" ("_")
+ "_Int" :: xnum => i ("_")
datatype
"bin" = Plus
--- a/src/ZF/ex/Brouwer.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Brouwer.thy Sat Dec 09 13:36:11 1995 +0100
@@ -10,8 +10,8 @@
Brouwer = InfDatatype +
consts
- brouwer :: "i"
- Well :: "[i,i=>i]=>i"
+ brouwer :: i
+ Well :: [i,i=>i]=>i
datatype <= "Vfrom(0, csucc(nat))"
"brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
--- a/src/ZF/ex/CoUnit.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/CoUnit.thy Sat Dec 09 13:36:11 1995 +0100
@@ -17,7 +17,7 @@
Coalgebra Theorem
*)
consts
- counit :: "i"
+ counit :: i
codatatype
"counit" = Con ("x: counit")
@@ -27,7 +27,7 @@
*)
consts
- counit2 :: "i"
+ counit2 :: i
codatatype
"counit2" = Con2 ("x: counit2", "y: counit2")
--- a/src/ZF/ex/Comb.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Comb.thy Sat Dec 09 13:36:11 1995 +0100
@@ -16,7 +16,7 @@
Comb = Datatype +
(** Datatype definition of combinators S and K, with infixed application **)
-consts comb :: "i"
+consts comb :: i
datatype (* <= "univ(0)" *)
"comb" = K
| S
@@ -26,9 +26,9 @@
and (multi-step) reductions, --->
**)
consts
- contract :: "i"
- "-1->" :: "[i,i] => o" (infixl 50)
- "--->" :: "[i,i] => o" (infixl 50)
+ contract :: i
+ "-1->" :: [i,i] => o (infixl 50)
+ "--->" :: [i,i] => o (infixl 50)
translations
"p -1-> q" == "<p,q> : contract"
@@ -48,9 +48,9 @@
and (multi-step) parallel reductions, ===>
**)
consts
- parcontract :: "i"
- "=1=>" :: "[i,i] => o" (infixl 50)
- "===>" :: "[i,i] => o" (infixl 50)
+ parcontract :: i
+ "=1=>" :: [i,i] => o (infixl 50)
+ "===>" :: [i,i] => o (infixl 50)
translations
"p =1=> q" == "<p,q> : parcontract"
@@ -68,8 +68,8 @@
(*Misc definitions*)
consts
- diamond :: "i => o"
- I :: "i"
+ diamond :: i => o
+ I :: i
defs
--- a/src/ZF/ex/Data.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Data.thy Sat Dec 09 13:36:11 1995 +0100
@@ -10,7 +10,7 @@
Data = Datatype +
consts
- data :: "[i,i] => i"
+ data :: [i,i] => i
datatype
"data(A,B)" = Con0
--- a/src/ZF/ex/Enum.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Enum.thy Sat Dec 09 13:36:11 1995 +0100
@@ -11,7 +11,7 @@
Enum = Datatype +
consts
- enum :: "i"
+ enum :: i
datatype
"enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
--- a/src/ZF/ex/Integ.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Integ.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,17 +8,17 @@
Integ = EquivClass + Arith +
consts
- intrel,integ:: "i"
- znat :: "i=>i" ("$# _" [80] 80)
- zminus :: "i=>i" ("$~ _" [80] 80)
- znegative :: "i=>o"
- zmagnitude :: "i=>i"
- "$*" :: "[i,i]=>i" (infixl 70)
- "$'/" :: "[i,i]=>i" (infixl 70)
- "$'/'/" :: "[i,i]=>i" (infixl 70)
- "$+" :: "[i,i]=>i" (infixl 65)
- "$-" :: "[i,i]=>i" (infixl 65)
- "$<" :: "[i,i]=>o" (infixl 50)
+ intrel,integ:: i
+ znat :: i=>i ("$# _" [80] 80)
+ zminus :: i=>i ("$~ _" [80] 80)
+ znegative :: i=>o
+ zmagnitude :: i=>i
+ "$*" :: [i,i]=>i (infixl 70)
+ "$'/" :: [i,i]=>i (infixl 70)
+ "$'/'/" :: [i,i]=>i (infixl 70)
+ "$+" :: [i,i]=>i (infixl 65)
+ "$-" :: [i,i]=>i (infixl 65)
+ "$<" :: [i,i]=>o (infixl 50)
defs
--- a/src/ZF/ex/LList.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/LList.thy Sat Dec 09 13:36:11 1995 +0100
@@ -17,7 +17,7 @@
LList = Datatype +
consts
- llist :: "i=>i"
+ llist :: i=>i
codatatype
"llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
@@ -25,7 +25,7 @@
(*Coinductive definition of equality*)
consts
- lleq :: "i=>i"
+ lleq :: i=>i
(*Previously used <*> in the domain and variant pairs as elements. But
standard pairs work just as well. To use variant pairs, must change prefix
@@ -40,8 +40,8 @@
(*Lazy list functions; flip is not definitional!*)
consts
- lconst :: "i => i"
- flip :: "i => i"
+ lconst :: i => i
+ flip :: i => i
defs
lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
--- a/src/ZF/ex/Limit.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Limit.thy Sat Dec 09 13:36:11 1995 +0100
@@ -21,43 +21,43 @@
consts
- "rel" :: "[i,i,i]=>o" (* rel(D,x,y) *)
- "set" :: "i=>i" (* set(D) *)
- "po" :: "i=>o" (* po(D) *)
- "chain" :: "[i,i]=>o" (* chain(D,X) *)
- "isub" :: "[i,i,i]=>o" (* isub(D,X,x) *)
- "islub" :: "[i,i,i]=>o" (* islub(D,X,x) *)
- "lub" :: "[i,i]=>i" (* lub(D,X) *)
- "cpo" :: "i=>o" (* cpo(D) *)
- "pcpo" :: "i=>o" (* pcpo(D) *)
- "bot" :: "i=>i" (* bot(D) *)
- "mono" :: "[i,i]=>i" (* mono(D,E) *)
- "cont" :: "[i,i]=>i" (* cont(D,E) *)
- "cf" :: "[i,i]=>i" (* cf(D,E) *)
+ "rel" :: [i,i,i]=>o (* rel(D,x,y) *)
+ "set" :: i=>i (* set(D) *)
+ "po" :: i=>o (* po(D) *)
+ "chain" :: [i,i]=>o (* chain(D,X) *)
+ "isub" :: [i,i,i]=>o (* isub(D,X,x) *)
+ "islub" :: [i,i,i]=>o (* islub(D,X,x) *)
+ "lub" :: [i,i]=>i (* lub(D,X) *)
+ "cpo" :: i=>o (* cpo(D) *)
+ "pcpo" :: i=>o (* pcpo(D) *)
+ "bot" :: i=>i (* bot(D) *)
+ "mono" :: [i,i]=>i (* mono(D,E) *)
+ "cont" :: [i,i]=>i (* cont(D,E) *)
+ "cf" :: [i,i]=>i (* cf(D,E) *)
- "suffix" :: "[i,i]=>i" (* suffix(X,n) *)
- "subchain" :: "[i,i]=>o" (* subchain(X,Y) *)
- "dominate" :: "[i,i,i]=>o" (* dominate(D,X,Y) *)
- "matrix" :: "[i,i]=>o" (* matrix(D,M) *)
+ "suffix" :: [i,i]=>i (* suffix(X,n) *)
+ "subchain" :: [i,i]=>o (* subchain(X,Y) *)
+ "dominate" :: [i,i,i]=>o (* dominate(D,X,Y) *)
+ "matrix" :: [i,i]=>o (* matrix(D,M) *)
- "projpair" :: "[i,i,i,i]=>o" (* projpair(D,E,e,p) *)
- "emb" :: "[i,i,i]=>o" (* emb(D,E,e) *)
- "Rp" :: "[i,i,i]=>i" (* Rp(D,E,e) *)
- "iprod" :: "i=>i" (* iprod(DD) *)
- "mkcpo" :: "[i,i=>o]=>i" (* mkcpo(D,P) *)
- "subcpo" :: "[i,i]=>o" (* subcpo(D,E) *)
- "subpcpo" :: "[i,i]=>o" (* subpcpo(D,E) *)
+ "projpair" :: [i,i,i,i]=>o (* projpair(D,E,e,p) *)
+ "emb" :: [i,i,i]=>o (* emb(D,E,e) *)
+ "Rp" :: [i,i,i]=>i (* Rp(D,E,e) *)
+ "iprod" :: i=>i (* iprod(DD) *)
+ "mkcpo" :: [i,i=>o]=>i (* mkcpo(D,P) *)
+ "subcpo" :: [i,i]=>o (* subcpo(D,E) *)
+ "subpcpo" :: [i,i]=>o (* subpcpo(D,E) *)
- "emb_chain" :: "[i,i]=>o" (* emb_chain(DD,ee) *)
- "Dinf" :: "[i,i]=>i" (* Dinf(DD,ee) *)
+ "emb_chain" :: [i,i]=>o (* emb_chain(DD,ee) *)
+ "Dinf" :: [i,i]=>i (* Dinf(DD,ee) *)
- "e_less" :: "[i,i,i,i]=>i" (* e_less(DD,ee,m,n) *)
- "e_gr" :: "[i,i,i,i]=>i" (* e_gr(DD,ee,m,n) *)
- "eps" :: "[i,i,i,i]=>i" (* eps(DD,ee,m,n) *)
- "rho_emb" :: "[i,i,i]=>i" (* rho_emb(DD,ee,n) *)
- "rho_proj" :: "[i,i,i]=>i" (* rho_proj(DD,ee,n) *)
- "commute" :: "[i,i,i,i=>i]=>o" (* commute(DD,ee,E,r) *)
- "mediating" :: "[i,i,i=>i,i=>i,i]=>o" (* mediating(E,G,r,f,t) *)
+ "e_less" :: [i,i,i,i]=>i (* e_less(DD,ee,m,n) *)
+ "e_gr" :: [i,i,i,i]=>i (* e_gr(DD,ee,m,n) *)
+ "eps" :: [i,i,i,i]=>i (* eps(DD,ee,m,n) *)
+ "rho_emb" :: [i,i,i]=>i (* rho_emb(DD,ee,n) *)
+ "rho_proj" :: [i,i,i]=>i (* rho_proj(DD,ee,n) *)
+ "commute" :: [i,i,i,i=>i]=>o (* commute(DD,ee,E,r) *)
+ "mediating" :: [i,i,i=>i,i=>i,i]=>o (* mediating(E,G,r,f,t) *)
rules
--- a/src/ZF/ex/ListN.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/ListN.thy Sat Dec 09 13:36:11 1995 +0100
@@ -10,7 +10,7 @@
*)
ListN = List +
-consts listn ::"i=>i"
+consts listn ::i=>i
inductive
domains "listn(A)" <= "nat*list(A)"
intrs
--- a/src/ZF/ex/Ntree.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Ntree.thy Sat Dec 09 13:36:11 1995 +0100
@@ -11,9 +11,9 @@
Ntree = InfDatatype +
consts
- ntree :: "i=>i"
- maptree :: "i=>i"
- maptree2 :: "[i,i] => i"
+ ntree :: i=>i
+ maptree :: i=>i
+ maptree2 :: [i,i] => i
datatype
"ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
--- a/src/ZF/ex/Primrec.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Primrec.thy Sat Dec 09 13:36:11 1995 +0100
@@ -16,14 +16,14 @@
Primrec = List +
consts
- primrec :: "i"
- SC :: "i"
- CONST :: "i=>i"
- PROJ :: "i=>i"
- COMP :: "[i,i]=>i"
- PREC :: "[i,i]=>i"
- ACK :: "i=>i"
- ack :: "[i,i]=>i"
+ primrec :: i
+ SC :: i
+ CONST :: i=>i
+ PROJ :: i=>i
+ COMP :: [i,i]=>i
+ PREC :: [i,i]=>i
+ ACK :: i=>i
+ ack :: [i,i]=>i
translations
"ack(x,y)" == "ACK(x) ` [y]"
--- a/src/ZF/ex/PropLog.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/PropLog.thy Sat Dec 09 13:36:11 1995 +0100
@@ -11,7 +11,7 @@
(** The datatype of propositions; note mixfix syntax **)
consts
- prop :: "i"
+ prop :: i
datatype
"prop" = Fls
@@ -20,8 +20,8 @@
(** The proof system **)
consts
- thms :: "i => i"
- "|-" :: "[i,i] => o" (infixl 50)
+ thms :: i => i
+ "|-" :: [i,i] => o (infixl 50)
translations
"H |- p" == "p : thms(H)"
@@ -39,10 +39,10 @@
(** The semantics **)
consts
- prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
- is_true :: "[i,i] => o"
- "|=" :: "[i,i] => o" (infixl 50)
- hyps :: "[i,i] => i"
+ prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
+ is_true :: [i,i] => o
+ "|=" :: [i,i] => o (infixl 50)
+ hyps :: [i,i] => i
defs
--- a/src/ZF/ex/Ramsey.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Ramsey.thy Sat Dec 09 13:36:11 1995 +0100
@@ -20,9 +20,9 @@
Ramsey = Arith +
consts
- Symmetric :: "i=>o"
- Atleast :: "[i,i]=>o"
- Clique,Indept,Ramsey :: "[i,i,i]=>o"
+ Symmetric :: i=>o
+ Atleast :: [i,i]=>o
+ Clique,Indept,Ramsey :: [i,i,i]=>o
defs
--- a/src/ZF/ex/Rmap.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Rmap.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
Rmap = List +
consts
- rmap :: "i=>i"
+ rmap :: i=>i
inductive
domains "rmap(r)" <= "list(domain(r))*list(range(r))"
--- a/src/ZF/ex/TF.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/TF.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,14 +8,14 @@
TF = List +
consts
- TF_rec :: "[i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i"
- TF_map :: "[i=>i, i] => i"
- TF_size :: "i=>i"
- TF_preorder :: "i=>i"
- list_of_TF :: "i=>i"
- TF_of_list :: "i=>i"
+ TF_rec :: [i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i
+ TF_map :: [i=>i, i] => i
+ TF_size :: i=>i
+ TF_preorder :: i=>i
+ list_of_TF :: i=>i
+ TF_of_list :: i=>i
- tree, forest, tree_forest :: "i=>i"
+ tree, forest, tree_forest :: i=>i
datatype
"tree(A)" = Tcons ("a: A", "f: forest(A)")
--- a/src/ZF/ex/Term.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Term.thy Sat Dec 09 13:36:11 1995 +0100
@@ -9,13 +9,13 @@
Term = List +
consts
- term_rec :: "[i, [i,i,i]=>i] => i"
- term_map :: "[i=>i, i] => i"
- term_size :: "i=>i"
- reflect :: "i=>i"
- preorder :: "i=>i"
+ term_rec :: [i, [i,i,i]=>i] => i
+ term_map :: [i=>i, i] => i
+ term_size :: i=>i
+ reflect :: i=>i
+ preorder :: i=>i
- term :: "i=>i"
+ term :: i=>i
datatype
"term(A)" = Apply ("a: A", "l: list(term(A))")