--- a/src/ZF/AC.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/AC.ML Fri Oct 10 18:23:31 1997 +0200
@@ -25,7 +25,7 @@
qed "AC_ball_Pi";
goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";
-by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
+by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
by (etac exI 2);
by (Blast_tac 1);
qed "AC_Pi_Pow";
@@ -33,7 +33,7 @@
val [nonempty] = goal AC.thy
"[| !!x. x:A ==> (EX y. y:x) \
\ |] ==> EX f: A->Union(A). ALL x:A. f`x : x";
-by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
+by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
by (etac nonempty 1);
by (blast_tac (!claset addDs [apply_type] addIs [Pi_type]) 1);
qed "AC_func";
--- a/src/ZF/AC/AC18_AC19.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/AC/AC18_AC19.ML Fri Oct 10 18:23:31 1997 +0200
@@ -47,7 +47,7 @@
val [prem] = goalw thy [AC18_def, AC19_def] "AC18 ==> AC19";
by (rtac allI 1);
-by (res_inst_tac [("B1","%x.x")] (forall_elim_vars 0 prem RS revcut_rl) 1);
+by (res_inst_tac [("B1","%x. x")] (forall_elim_vars 0 prem RS revcut_rl) 1);
by (Fast_tac 1);
qed "AC18_AC19";
--- a/src/ZF/AC/Cardinal_aux.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML Fri Oct 10 18:23:31 1997 +0200
@@ -187,7 +187,7 @@
goalw thy [eqpoll_def] "!!A B. A Int B = 0 ==> A Un B eqpoll A + B";
by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1);
-by (res_inst_tac [("d","%z. case(%x.x, %x.x, z)")] lam_bijective 1);
+by (res_inst_tac [("d","%z. case(%x. x, %x. x, z)")] lam_bijective 1);
by (fast_tac (!claset addSIs [if_type, InlI, InrI]) 1);
by (TRYALL (etac sumE ));
by (TRYALL (split_tac [expand_if]));
--- a/src/ZF/AC/WO6_WO1.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Fri Oct 10 18:23:31 1997 +0200
@@ -244,7 +244,7 @@
"!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
\ domain(uu(f,b,g,d)) eqpoll succ(m); \
\ ALL b<a. f`b lepoll succ(m); y*y<=y; \
-\ (UN b<a.f`b)=y; Ord(a); m:nat; s:f`b; b<a \
+\ (UN b<a. f`b)=y; Ord(a); m:nat; s:f`b; b<a \
\ |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
by (dtac sym 1);
by (asm_simp_tac
--- a/src/ZF/Arith.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Arith.ML Fri Oct 10 18:23:31 1997 +0200
@@ -489,7 +489,7 @@
(*le monotonicity, 1st argument*)
goal Arith.thy
"!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
-by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
+by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
qed "add_le_mono1";
--- a/src/ZF/Arith.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Arith.thy Fri Oct 10 18:23:31 1997 +0200
@@ -18,8 +18,8 @@
defs
rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
- add_def "m#+n == rec(m, n, %u v.succ(v))"
- diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
+ add_def "m#+n == rec(m, n, %u v. succ(v))"
+ diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y. x))"
mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
mod_def "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
div_def "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
--- a/src/ZF/Cardinal.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Cardinal.ML Fri Oct 10 18:23:31 1997 +0200
@@ -187,7 +187,7 @@
(** LEAST -- the least number operator [from HOL/Univ.ML] **)
val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]
- "[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (LEAST x.P(x)) = i";
+ "[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i";
by (rtac the_equality 1);
by (blast_tac (!claset addSIs [premP,premOrd,premNot]) 1);
by (REPEAT (etac conjE 1));
@@ -195,7 +195,7 @@
by (ALLGOALS (blast_tac (!claset addSIs [premP] addSDs [premNot])));
qed "Least_equality";
-goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> P(LEAST x.P(x))";
+goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> P(LEAST x. P(x))";
by (etac rev_mp 1);
by (trans_ind_tac "i" [] 1);
by (rtac impI 1);
@@ -206,7 +206,7 @@
qed "LeastI";
(*Proof is almost identical to the one above!*)
-goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> (LEAST x.P(x)) le i";
+goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> (LEAST x. P(x)) le i";
by (etac rev_mp 1);
by (trans_ind_tac "i" [] 1);
by (rtac impI 1);
@@ -217,7 +217,7 @@
qed "Least_le";
(*LEAST really is the smallest*)
-goal Cardinal.thy "!!i. [| P(i); i < (LEAST x.P(x)) |] ==> Q";
+goal Cardinal.thy "!!i. [| P(i); i < (LEAST x. P(x)) |] ==> Q";
by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1);
by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
qed "less_LeastE";
@@ -232,12 +232,12 @@
(*If there is no such P then LEAST is vacuously 0*)
goalw Cardinal.thy [Least_def]
- "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x.P(x)) = 0";
+ "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x. P(x)) = 0";
by (rtac the_0 1);
by (Blast_tac 1);
qed "Least_0";
-goal Cardinal.thy "Ord(LEAST x.P(x))";
+goal Cardinal.thy "Ord(LEAST x. P(x))";
by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1);
by (safe_tac (!claset));
by (rtac (Least_le RS ltE) 2);
@@ -251,7 +251,7 @@
(*Not needed for simplification, but helpful below*)
val prems = goal Cardinal.thy
- "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))";
+ "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x. P(x)) = (LEAST x. Q(x))";
by (simp_tac (!simpset addsimps prems) 1);
qed "Least_cong";
@@ -570,7 +570,7 @@
"!!A B. [| A lepoll B; b ~: B |] ==> cons(a,A) lepoll cons(b,B)";
by (safe_tac (!claset));
by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1);
-by (res_inst_tac [("d","%z.if(z:B, converse(f)`z, a)")]
+by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, a)")]
lam_injective 1);
by (asm_simp_tac (!simpset addsimps [inj_is_fun RS apply_type, cons_iff]
setloop etac consE') 1);
--- a/src/ZF/CardinalArith.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/CardinalArith.ML Fri Oct 10 18:23:31 1997 +0200
@@ -103,8 +103,8 @@
goalw CardinalArith.thy [eqpoll_def] "succ(A)+B eqpoll succ(A+B)";
by (rtac exI 1);
-by (res_inst_tac [("c", "%z.if(z=Inl(A),A+B,z)"),
- ("d", "%z.if(z=A+B,Inl(A),z)")]
+by (res_inst_tac [("c", "%z. if(z=Inl(A),A+B,z)"),
+ ("d", "%z. if(z=A+B,Inl(A),z)")]
lam_bijective 1);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [succI2, mem_imp_not_eq]
@@ -269,7 +269,7 @@
goalw CardinalArith.thy [eqpoll_def] "succ(A)*B eqpoll B + A*B";
by (rtac exI 1);
by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"),
- ("d", "case(%y. <A,y>, %z.z)")]
+ ("d", "case(%y. <A,y>, %z. z)")]
lam_bijective 1);
by (safe_tac (!claset addSEs [sumE]));
by (ALLGOALS
@@ -315,7 +315,7 @@
"lam z:cons(u,A). if(z=u, f`0, \
\ if(z: range(f), f`succ(converse(f)`z), z))")] exI 1);
by (res_inst_tac [("d", "%y. if(y: range(f), \
-\ nat_case(u, %z.f`z, converse(f)`y), y)")]
+\ nat_case(u, %z. f`z, converse(f)`y), y)")]
lam_injective 1);
by (fast_tac (!claset addSIs [if_type, nat_succI, apply_type]
addIs [inj_is_fun, inj_converse_fun]) 1);
--- a/src/ZF/Coind/Map.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Map.ML Fri Oct 10 18:23:31 1997 +0200
@@ -18,7 +18,7 @@
by (Fast_tac 1);
qed "qbeta_emp";
-goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
+goal Map.thy "!!A. a ~: A ==> Sigma(A,B)``{a}=0";
by (Fast_tac 1);
qed "image_Sigma1";
@@ -44,7 +44,7 @@
(* Theorems *)
val prems = goalw Map.thy [PMap_def,TMap_def]
- "[| m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) |] ==> m:quniv(B)";
+ "[| m:PMap(A,quniv(B)); !!x. x:A ==> x:univ(B) |] ==> m:quniv(B)";
by (cut_facts_tac prems 1);
by (rtac (MapQU_lemma RS subsetD) 1);
by (rtac subsetI 1);
@@ -56,7 +56,7 @@
(* Monotonicity *)
(* ############################################################ *)
-goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
+goalw Map.thy [PMap_def,TMap_def] "!!A. B<=C ==> PMap(A,B)<=PMap(A,C)";
by (Fast_tac 1);
qed "map_mono";
@@ -139,11 +139,11 @@
(* Lemmas *)
-goal Map.thy "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
+goal Map.thy "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))";
by (Fast_tac 1);
qed "domain_UN";
-goal Map.thy "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
+goal Map.thy "domain(Sigma(A,B)) = {x:A. EX y. y:B(x)}";
by (simp_tac (!simpset addsimps [domain_UN,domain_0,domain_cons]) 1);
by (Fast_tac 1);
qed "domain_Sigma";
@@ -155,7 +155,7 @@
qed "map_domain_emp";
goalw Map.thy [map_owr_def]
- "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
+ "!!a. b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
by (simp_tac (!simpset addsimps [domain_Sigma]) 1);
by (rtac equalityI 1);
by (Fast_tac 1);
@@ -179,7 +179,7 @@
qed "map_app_owr1";
goalw Map.thy [map_app_def,map_owr_def]
- "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
+ "!!a. c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
by (rtac (excluded_middle RS disjE) 1);
by (stac qbeta_emp 1);
by (assume_tac 1);
--- a/src/ZF/Coind/Map.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Map.thy Fri Oct 10 18:23:31 1997 +0200
@@ -10,7 +10,7 @@
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}"
+ 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))"
(* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
--- a/src/ZF/Coind/Types.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Types.thy Fri Oct 10 18:23:31 1997 +0200
@@ -27,14 +27,14 @@
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))"
+ 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
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))"
+ 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))"
end
--- a/src/ZF/Coind/Values.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Values.ML Fri Oct 10 18:23:31 1997 +0200
@@ -42,7 +42,7 @@
(* Nonempty sets *)
-val prems = goal Values.thy "A ~= 0 ==> EX a.a:A";
+val prems = goal Values.thy "A ~= 0 ==> EX a. a:A";
by (cut_facts_tac prems 1);
by (rtac (foundation RS disjE) 1);
by (Fast_tac 1);
@@ -60,7 +60,7 @@
qed "v_closNE";
goalw Values.thy (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
- "!!c.c:Const ==> v_const(c) ~= 0";
+ "!!c. c:Const ==> v_const(c) ~= 0";
by (dtac constNEE 1);
by (etac not_emptyE 1);
by (rtac not_emptyI 1);
@@ -75,7 +75,7 @@
(* Proving that the empty set is not a value *)
-goal Values.thy "!!v.v:Val ==> v ~= 0";
+goal Values.thy "!!v. v:Val ==> v ~= 0";
by (etac ValE 1);
by (ALLGOALS hyp_subst_tac);
by (etac v_constNE 1);
@@ -102,7 +102,7 @@
qed "ve_app_owr1";
goalw Values.thy [ve_app_def,ve_owr_def]
- "!!ve.ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
+ "!!ve. ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
by (etac ValEnvE 1);
by (asm_full_simp_tac (!simpset addsimps Val_ValEnv.case_eqns) 1);
by (rtac map_app_owr2 1);
--- a/src/ZF/Coind/Values.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Values.thy Fri Oct 10 18:23:31 1997 +0200
@@ -27,11 +27,11 @@
ve_emp_def "ve_emp == ve_mk(map_emp)"
ve_owr_def
"ve_owr(ve,x,v) ==
- ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
+ ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m. map_owr(m,x,v),ve))"
ve_dom_def
- "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)"
+ "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m. domain(m),ve)"
ve_app_def
- "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m.map_app(m,a),ve)"
+ "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m. map_app(m,a),ve)"
end
--- a/src/ZF/EquivClass.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/EquivClass.ML Fri Oct 10 18:23:31 1997 +0200
@@ -238,7 +238,7 @@
(*Obsolete?*)
val [equivA,ZinA,congt,commute] = goalw EquivClass.thy [quotient_def]
"[| equiv(A,r); Z: A/r; \
-\ !!w. [| w: A |] ==> congruent(r, %z.b(w,z)); \
+\ !!w. [| w: A |] ==> congruent(r, %z. b(w,z)); \
\ !!x y. [| x: A; y: A |] ==> b(y,x) = b(x,y) \
\ |] ==> congruent(r, %w. UN z: Z. b(w,z))";
val congt' = rewrite_rule [congruent_def] congt;
--- a/src/ZF/List.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/List.ML Fri Oct 10 18:23:31 1997 +0200
@@ -265,13 +265,13 @@
(*** theorems about map ***)
val prems = goal List.thy
- "l: list(A) ==> map(%u.u, l) = l";
+ "l: list(A) ==> map(%u. u, l) = l";
by (list_ind_tac "l" prems 1);
by (ALLGOALS Asm_simp_tac);
qed "map_ident";
val prems = goal List.thy
- "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
+ "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
by (list_ind_tac "l" prems 1);
by (ALLGOALS Asm_simp_tac);
qed "map_compose";
--- a/src/ZF/List.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/List.thy Fri Oct 10 18:23:31 1997 +0200
@@ -31,16 +31,16 @@
constdefs
hd :: i=>i
- "hd(l) == list_case(0, %x xs.x, l)"
+ "hd(l) == list_case(0, %x xs. x, l)"
tl :: i=>i
- "tl(l) == list_case(Nil, %x xs.xs, l)"
+ "tl(l) == list_case(Nil, %x xs. xs, l)"
drop :: [i,i]=>i
"drop(i,l) == rec(i, l, %j r. tl(r))"
list_rec :: [i, i, [i,i,i]=>i] => i
- "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
+ "list_rec(l,c,h) == Vrec(l, %l g. list_case(c, %x xs. h(x, xs, g`xs), l))"
map :: [i=>i, i] => i
"map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))"
--- a/src/ZF/OrdQuant.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/OrdQuant.ML Fri Oct 10 18:23:31 1997 +0200
@@ -49,7 +49,7 @@
(*Not of the general form for such rules; ~EX has become ALL~ *)
qed_goal "oexCI" thy
- "[| ALL x<A. ~P(x) ==> P(a); a<A |] ==> EX x<A.P(x)"
+ "[| ALL x<A. ~P(x) ==> P(a); a<A |] ==> EX x<A. P(x)"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ]);
@@ -85,7 +85,7 @@
(fn _=> [ (fast_tac (!claset addIs [OUN_I] addSEs [OUN_E]) 1) ]);
qed_goal "OUN_cong" thy
- "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i.C(x)) = (UN x<j.D(x))"
+ "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
(fn prems=>
[ rtac equality_iffI 1,
simp_tac (!simpset addcongs [oex_cong] addsimps (OUN_iff::prems)) 1 ]);
--- a/src/ZF/OrderArith.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/OrderArith.ML Fri Oct 10 18:23:31 1997 +0200
@@ -136,7 +136,7 @@
ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
goal OrderArith.thy
"!!A B. A Int B = 0 ==> \
-\ (lam z:A+B. case(%x.x, %y.y, z)) : bij(A+B, A Un B)";
+\ (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")]
lam_bijective 1);
by (blast_tac (!claset addSIs [if_type]) 2);
@@ -149,15 +149,15 @@
(** Associativity **)
goal OrderArith.thy
- "(lam z:(A+B)+C. case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
+ "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
\ : bij((A+B)+C, A+(B+C))";
-by (res_inst_tac [("d", "case(%x.Inl(Inl(x)), case(%x.Inl(Inr(x)), Inr))")]
+by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")]
lam_bijective 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop etac sumE)));
qed "sum_assoc_bij";
goal OrderArith.thy
- "(lam z:(A+B)+C. case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
+ "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
\ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), \
\ A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
@@ -283,7 +283,7 @@
case_cong, id_conv, comp_lam, case_case.*)
goal OrderArith.thy
"!!a. a~:C ==> \
-\ (lam x:C*B + D. case(%x.x, %y.<a,y>, x)) \
+\ (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) \
\ : bij(C*B + D, C*B Un {a}*D)";
by (rtac subst_elem 1);
by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
@@ -298,7 +298,7 @@
goal OrderArith.thy
"!!A. [| a:A; well_ord(A,r) |] ==> \
-\ (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x.x, %y.<a,y>, x)) \
+\ (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) \
\ : ord_iso(pred(A,a,r)*B + pred(B,b,s), \
\ radd(A*B, rmult(A,r,B,s), B, s), \
\ pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))";
@@ -314,7 +314,7 @@
(** Distributive law **)
goal OrderArith.thy
- "(lam <x,z>:(A+B)*C. case(%y.Inl(<y,z>), %y.Inr(<y,z>), x)) \
+ "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
\ : bij((A+B)*C, (A*C)+(B*C))";
by (res_inst_tac
[("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
@@ -323,7 +323,7 @@
qed "sum_prod_distrib_bij";
goal OrderArith.thy
- "(lam <x,z>:(A+B)*C. case(%y.Inl(<y,z>), %y.Inr(<y,z>), x)) \
+ "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
\ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
\ (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
--- a/src/ZF/OrderType.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/OrderType.ML Fri Oct 10 18:23:31 1997 +0200
@@ -310,7 +310,7 @@
(** Addition with 0 **)
-goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)";
+goal OrderType.thy "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)";
by (res_inst_tac [("d", "Inl")] lam_bijective 1);
by (safe_tac (!claset));
by (ALLGOALS Asm_simp_tac);
@@ -323,7 +323,7 @@
by (fast_tac (!claset addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
qed "ordertype_sum_0_eq";
-goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)";
+goal OrderType.thy "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)";
by (res_inst_tac [("d", "Inr")] lam_bijective 1);
by (safe_tac (!claset));
by (ALLGOALS Asm_simp_tac);
@@ -343,7 +343,7 @@
"!!A B. a:A ==> \
\ (lam x:pred(A,a,r). Inl(x)) \
\ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
-by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
+by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
by (safe_tac (!claset));
by (ALLGOALS
(asm_full_simp_tac
@@ -363,7 +363,7 @@
"!!A B. b:B ==> \
\ id(A+pred(B,b,s)) \
\ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
-by (res_inst_tac [("d", "%z.z")] lam_bijective 1);
+by (res_inst_tac [("d", "%z. z")] lam_bijective 1);
by (safe_tac (!claset));
by (ALLGOALS (Asm_full_simp_tac));
qed "pred_Inr_bij";
@@ -592,7 +592,7 @@
goal OrderType.thy
"!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
-by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
+by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
by (blast_tac (!claset addSIs [if_type]) 1);
by (fast_tac (!claset addSIs [case_type]) 1);
by (etac sumE 2);
--- a/src/ZF/Perm.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Perm.ML Fri Oct 10 18:23:31 1997 +0200
@@ -37,7 +37,7 @@
"[| !!x. x:A ==> c(x): B; \
\ !!y. y:B ==> d(y): A; \
\ !!y. y:B ==> c(d(y)) = y \
-\ |] ==> (lam x:A.c(x)) : surj(A,B)";
+\ |] ==> (lam x:A. c(x)) : surj(A,B)";
by (res_inst_tac [("d", "d")] f_imp_surjective 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps ([lam_type]@prems)) ));
qed "lam_surjective";
@@ -77,7 +77,7 @@
val prems = goal Perm.thy
"[| !!x. x:A ==> c(x): B; \
\ !!x. x:A ==> d(c(x)) = x \
-\ |] ==> (lam x:A.c(x)) : inj(A,B)";
+\ |] ==> (lam x:A. c(x)) : inj(A,B)";
by (res_inst_tac [("d", "d")] f_imp_injective 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps ([lam_type]@prems)) ));
qed "lam_injective";
@@ -100,7 +100,7 @@
\ !!y. y:B ==> d(y): A; \
\ !!x. x:A ==> d(c(x)) = x; \
\ !!y. y:B ==> c(d(y)) = y \
-\ |] ==> (lam x:A.c(x)) : bij(A,B)";
+\ |] ==> (lam x:A. c(x)) : bij(A,B)";
by (REPEAT (ares_tac (prems @ [IntI, lam_injective, lam_surjective]) 1));
qed "lam_bijective";
@@ -329,7 +329,7 @@
(*Simplifies compositions of lambda-abstractions*)
val [prem] = goal Perm.thy
"[| !!x. x:A ==> b(x): B \
-\ |] ==> (lam y:B.c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
+\ |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
by (rtac fun_extension 1);
by (rtac comp_fun 1);
by (rtac lam_funtype 2);
@@ -427,7 +427,7 @@
"!!f A B. [| f: A->B; g: B->A |] ==> \
\ f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
by (safe_tac (!claset));
-by (dres_inst_tac [("t", "%h.h`y ")] subst_context 1);
+by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1);
by (Asm_full_simp_tac 1);
by (rtac fun_extension 1);
by (REPEAT (ares_tac [comp_fun, lam_type] 1));
--- a/src/ZF/QPair.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/QPair.ML Fri Oct 10 18:23:31 1997 +0200
@@ -125,7 +125,7 @@
(*A META-equality, so that it applies to higher types as well...*)
qed_goalw "qsplit" thy [qsplit_def]
- "qsplit(%x y.c(x,y), <a;b>) == c(a,b)"
+ "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
(fn _ => [ (Simp_tac 1),
(rtac reflexive_thm 1) ]);
@@ -134,7 +134,7 @@
qed_goal "qsplit_type" thy
"[| p:QSigma(A,B); \
\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
-\ |] ==> qsplit(%x y.c(x,y), p) : C(p)"
+\ |] ==> qsplit(%x y. c(x,y), p) : C(p)"
(fn major::prems=>
[ (rtac (major RS QSigmaE) 1),
(asm_simp_tac (!simpset addsimps prems) 1) ]);
@@ -322,7 +322,7 @@
by (Blast_tac 1);
qed "Part_QInr";
-goal thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
+goal thy "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}";
by (Blast_tac 1);
qed "Part_QInr2";
--- a/src/ZF/Resid/Confluence.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Confluence.ML Fri Oct 10 18:23:31 1997 +0200
@@ -21,7 +21,7 @@
goalw Confluence.thy [confluence_def,strip_def]
- "!!u.strip==> confluence(Spar_red)";
+ "!!u. strip==> confluence(Spar_red)";
by (resolve_tac [impI RS allI RS allI] 1);
by (etac Spar_red.induct 1);
by (Fast_tac 1);
--- a/src/ZF/Resid/Conversion.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Conversion.ML Fri Oct 10 18:23:31 1997 +0200
@@ -10,7 +10,7 @@
AddIs (Sconv.intrs @ Sconv1.intrs);
goal Conversion.thy
- "!!u.m<--->n ==> n<--->m";
+ "!!u. m<--->n ==> n<--->m";
by (etac Sconv.induct 1);
by (etac Sconv1.induct 1);
by (ALLGOALS Blast_tac);
@@ -21,7 +21,7 @@
(* ------------------------------------------------------------------------- *)
goal Conversion.thy
- "!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)";
+ "!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)";
by (etac Sconv.induct 1);
by (etac Sconv1.induct 1);
by (blast_tac (!claset addIs [red1D1,redD2]) 1);
--- a/src/ZF/Resid/Cube.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Cube.ML Fri Oct 10 18:23:31 1997 +0200
@@ -18,8 +18,8 @@
(* Having more assumptions than needed -- removed below *)
goal Cube.thy
- "!!u.v<==u ==> \
-\ regular(u)-->(ALL w.w~v-->w~u--> \
+ "!!u. v<==u ==> \
+\ regular(u)-->(ALL w. w~v-->w~u--> \
\ w |> u = (w|>v) |> (u|>v))";
by (etac Ssub.induct 1);
by (ALLGOALS (asm_simp_tac prism_ss));
--- a/src/ZF/Resid/Redex.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Redex.thy Fri Oct 10 18:23:31 1997 +0200
@@ -22,7 +22,7 @@
defs
redex_rec_def
"redex_rec(p,b,c,d) ==
- Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),
- %n x y.d(n, x, y, g`x, g`y), p))"
+ Vrec(p, %p g. redexes_case(b, %x. c(x,g`x),
+ %n x y. d(n, x, y, g`x, g`y), p))"
end
--- a/src/ZF/Resid/Reduction.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Reduction.ML Fri Oct 10 18:23:31 1997 +0200
@@ -76,23 +76,23 @@
(* ------------------------------------------------------------------------- *)
-goal Reduction.thy "!!u.m:lambda==> m =1=> m";
+goal Reduction.thy "!!u. m:lambda==> m =1=> m";
by (eresolve_tac [lambda.induct] 1);
by (ALLGOALS (Asm_simp_tac ));
qed "refl_par_red1";
-goal Reduction.thy "!!u.m-1->n ==> m=1=>n";
+goal Reduction.thy "!!u. m-1->n ==> m=1=>n";
by (etac Sred1.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [refl_par_red1]) ));
qed "red1_par_red1";
-goal Reduction.thy "!!u.m--->n ==> m===>n";
+goal Reduction.thy "!!u. m--->n ==> m===>n";
by (etac Sred.induct 1);
by (resolve_tac [Spar_red.trans] 3);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [refl_par_red1,red1_par_red1]) ));
qed "red_par_red";
-goal Reduction.thy "!!u.m===>n ==> m--->n";
+goal Reduction.thy "!!u. m===>n ==> m--->n";
by (etac Spar_red.induct 1);
by (etac Spar_red1.induct 1);
by (resolve_tac [Sred.trans] 5);
@@ -105,7 +105,7 @@
(* ------------------------------------------------------------------------- *)
goal Reduction.thy
- "!!u.m=1=>n ==> EX v. m|>v = n & m~v & regular(v)";
+ "!!u. m=1=>n ==> EX v. m|>v = n & m~v & regular(v)";
by (etac Spar_red1.induct 1);
by Safe_tac;
by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
@@ -119,14 +119,14 @@
(* ------------------------------------------------------------------------- *)
goal Reduction.thy
- "!!u.u:redexes ==> \
+ "!!u. u:redexes ==> \
\ ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS (asm_full_simp_tac (addsplit (!simpset))));
qed "unmmark_lift_rec";
goal Reduction.thy
- "!!u.v:redexes ==> ALL k:nat.ALL u:redexes. \
+ "!!u. v:redexes ==> ALL k:nat. ALL u:redexes. \
\ unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS (asm_full_simp_tac
@@ -139,7 +139,7 @@
(* ------------------------------------------------------------------------- *)
goal Reduction.thy
- "!!u.u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
+ "!!u. u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
by (etac Scomp.induct 1);
by (ALLGOALS (asm_full_simp_tac (reducL_ss addsimps [unmmark_subst_rec]) ));
by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
--- a/src/ZF/Resid/Residuals.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Residuals.ML Fri Oct 10 18:23:31 1997 +0200
@@ -44,13 +44,13 @@
(* ------------------------------------------------------------------------- *)
goal Residuals.thy
- "!!u.residuals(u,v,w) ==> ALL w1.residuals(u,v,w1) --> w1 = w";
+ "!!u. residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w";
by (etac Sres.induct 1);
by (ALLGOALS Fast_tac);
qed_spec_mp "residuals_function";
goal Residuals.thy
- "!!u.u~v ==> regular(v) --> (EX w.residuals(u,v,w))";
+ "!!u. u~v ==> regular(v) --> (EX w. residuals(u,v,w))";
by (etac Scomp.induct 1);
by (ALLGOALS Fast_tac);
qed "residuals_intro";
@@ -74,7 +74,7 @@
addSEs [comp_resfuncE]);
goalw Residuals.thy [res_func_def]
- "!!n.n:nat ==> Var(n) |> Var(n) = Var(n)";
+ "!!n. n:nat ==> Var(n) |> Var(n) = Var(n)";
by (fast_tac resfunc_cs 1);
qed "res_Var";
@@ -119,13 +119,13 @@
(* ------------------------------------------------------------------------- *)
goal Residuals.thy
- "!!u.u<==v ==> u~v";
+ "!!u. u<==v ==> u~v";
by (etac Ssub.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "sub_comp";
goal Residuals.thy
- "!!u.u<==v ==> regular(v) --> regular(u)";
+ "!!u. u<==v ==> regular(v) --> regular(u)";
by (etac Ssub.induct 1);
by (ALLGOALS (asm_simp_tac res1L_ss));
qed "sub_preserve_reg";
@@ -136,13 +136,13 @@
by (etac Scomp.induct 1);
by Safe_tac;
by (ALLGOALS (asm_full_simp_tac ((addsplit (!simpset)) addsimps [lift_subst])));
-by (dres_inst_tac [("psi", "ALL x:nat.Fun(?u(x)) |> ?v(x) = ?w(x)")] asm_rl 1);
+by (dres_inst_tac [("psi", "ALL x:nat. Fun(?u(x)) |> ?v(x) = ?w(x)")] asm_rl 1);
by (Asm_full_simp_tac 1);
qed "residuals_lift_rec";
goal Residuals.thy
- "!!u.u1~u2 ==> ALL v1 v2.v1~v2 --> regular(v2) --> regular(u2) -->\
-\ (ALL n:nat.subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
+ "!!u. u1~u2 ==> ALL v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
+\ (ALL n:nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
\ subst_rec(v1 |> v2, u1 |> u2,n))";
by (etac Scomp.induct 1);
by Safe_tac;
@@ -164,7 +164,7 @@
(* ------------------------------------------------------------------------- *)
goal Residuals.thy
- "!!u.u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
+ "!!u. u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
by (etac Scomp.induct 1);
by (ALLGOALS (asm_simp_tac res1L_ss));
by (dresolve_tac [spec RS mp RS mp RS mp] 1
@@ -176,7 +176,7 @@
goal Residuals.thy
- "!!u.u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
+ "!!u. u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
by (etac Scomp.induct 1);
by (safe_tac (!claset));
by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
@@ -188,13 +188,13 @@
(* ------------------------------------------------------------------------- *)
goal Residuals.thy
- "!!u.u~v ==> v ~ (u un v)";
+ "!!u. u~v ==> v ~ (u un v)";
by (etac Scomp.induct 1);
by (ALLGOALS Asm_full_simp_tac);
qed "union_preserve_comp";
goal Residuals.thy
- "!!u.u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
+ "!!u. u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
by (etac Scomp.induct 1);
by (safe_tac (!claset));
by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
--- a/src/ZF/Resid/Residuals.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Residuals.thy Fri Oct 10 18:23:31 1997 +0200
@@ -31,6 +31,6 @@
type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
rules
- res_func_def "u |> v == THE w.residuals(u,v,w)"
+ res_func_def "u |> v == THE w. residuals(u,v,w)"
end
--- a/src/ZF/Resid/SubUnion.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/SubUnion.ML Fri Oct 10 18:23:31 1997 +0200
@@ -22,7 +22,7 @@
(* ------------------------------------------------------------------------- *)
goalw SubUnion.thy [union_def]
- "!!u.n:nat==>Var(n) un Var(n)=Var(n)";
+ "!!u. n:nat==>Var(n) un Var(n)=Var(n)";
by (Asm_simp_tac 1);
by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
qed "union_Var";
@@ -65,13 +65,13 @@
(* comp proofs *)
(* ------------------------------------------------------------------------- *)
-goal SubUnion.thy "!!u.u:redexes ==> u ~ u";
+goal SubUnion.thy "!!u. u:redexes ==> u ~ u";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS Fast_tac);
qed "comp_refl";
goal SubUnion.thy
- "!!u.u ~ v ==> v ~ u";
+ "!!u. u ~ v ==> v ~ u";
by (etac Scomp.induct 1);
by (ALLGOALS Fast_tac);
qed "comp_sym";
@@ -83,7 +83,7 @@
goal SubUnion.thy
- "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w";
+ "!!u. u ~ v ==> ALL w. v ~ w-->u ~ w";
by (etac Scomp.induct 1);
by (ALLGOALS Fast_tac);
qed_spec_mp "comp_trans";
@@ -93,21 +93,21 @@
(* ------------------------------------------------------------------------- *)
goal SubUnion.thy
- "!!u.u ~ v ==> u <== (u un v)";
+ "!!u. u ~ v ==> u <== (u un v)";
by (etac Scomp.induct 1);
by (etac boolE 3);
by (ALLGOALS Asm_full_simp_tac);
qed "union_l";
goal SubUnion.thy
- "!!u.u ~ v ==> v <== (u un v)";
+ "!!u. u ~ v ==> v <== (u un v)";
by (etac Scomp.induct 1);
by (eres_inst_tac [("c","b2")] boolE 3);
by (ALLGOALS Asm_full_simp_tac);
qed "union_r";
goal SubUnion.thy
- "!!u.u ~ v ==> u un v = v un u";
+ "!!u. u ~ v ==> u un v = v un u";
by (etac Scomp.induct 1);
by (ALLGOALS(asm_simp_tac (!simpset addsimps [or_commute])));
qed "union_sym";
@@ -117,7 +117,7 @@
(* ------------------------------------------------------------------------- *)
goal SubUnion.thy
- "!!u.u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
+ "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
by (etac Scomp.induct 1);
by (ALLGOALS(asm_full_simp_tac
(!simpset setloop(SELECT_GOAL (safe_tac (!claset))))));
--- a/src/ZF/Resid/SubUnion.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/SubUnion.thy Fri Oct 10 18:23:31 1997 +0200
@@ -51,9 +51,8 @@
defs
union_def "u un v == redex_rec(u,
- %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),
- %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),
-%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,
+ %i. lam t:redexes. redexes_case(%j. Var(i), %x.0, %b x y.0, t),
+ %x m. lam t:redexes. redexes_case(%j.0, %y. Fun(m`y), %b y z.0, t),
+%b x y m p. lam t:redexes. redexes_case(%j.0, %y.0,
%c z u. App(b or c, m`z, p`u), t))`v"
end
-
--- a/src/ZF/Resid/Substitution.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Substitution.ML Fri Oct 10 18:23:31 1997 +0200
@@ -113,7 +113,7 @@
goal Substitution.thy
- "!!n.u:redexes ==> ALL k:nat.lift_rec(u,k):redexes";
+ "!!n. u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS(asm_full_simp_tac
((addsplit (!simpset)) addsimps [lift_rec_Fun,lift_rec_App])));
@@ -121,7 +121,7 @@
val lift_rec_type = lift_rec_type_a RS bspec;
goalw Substitution.thy []
- "!!n.v:redexes ==> ALL n:nat.ALL u:redexes.subst_rec(u,v,n):redexes";
+ "!!n. v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS(asm_full_simp_tac
((addsplit (!simpset)) addsimps [subst_Fun,subst_App,
@@ -140,7 +140,7 @@
(* ------------------------------------------------------------------------- *)
goalw Substitution.thy []
- "!!n.u:redexes ==> ALL n:nat.ALL i:nat.i le n --> \
+ "!!n. u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \
\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
by ((eresolve_tac [redexes.induct] 1)
THEN (ALLGOALS Asm_simp_tac));
@@ -159,8 +159,8 @@
qed "lift_lift";
goal Substitution.thy
- "!!n.v:redexes ==> \
-\ ALL n:nat.ALL m:nat.ALL u:redexes.n le m-->\
+ "!!n. v:redexes ==> \
+\ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\
\ lift_rec(subst_rec(u,v,n),m) = \
\ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
by ((eresolve_tac [redexes.induct] 1)
@@ -186,8 +186,8 @@
goalw Substitution.thy []
- "!!n.v:redexes ==> \
-\ ALL n:nat.ALL m:nat.ALL u:redexes.m le n-->\
+ "!!n. v:redexes ==> \
+\ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\
\ lift_rec(subst_rec(u,v,n),m) = \
\ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
by ((eresolve_tac [redexes.induct] 1)
@@ -208,8 +208,8 @@
goalw Substitution.thy []
- "!!n.u:redexes ==> \
-\ ALL n:nat.ALL v:redexes.subst_rec(v,lift_rec(u,n),n) = u";
+ "!!n. u:redexes ==> \
+\ ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) = u";
by ((eresolve_tac [redexes.induct] 1)
THEN (ALLGOALS Asm_simp_tac));
by Safe_tac;
@@ -220,8 +220,8 @@
qed "subst_rec_lift_rec";
goal Substitution.thy
- "!!n.v:redexes ==> \
-\ ALL m:nat.ALL n:nat.ALL u:redexes.ALL w:redexes.m le n --> \
+ "!!n. v:redexes ==> \
+\ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \
\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
\ subst_rec(w,subst_rec(u,v,m),n)";
by ((eresolve_tac [redexes.induct] 1) THEN
@@ -263,13 +263,13 @@
goal Substitution.thy
- "!!n.[|n:nat; u ~ v|]==> ALL m:nat.lift_rec(u,m) ~ lift_rec(v,m)";
+ "!!n.[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)";
by (etac Scomp.induct 1);
by (ALLGOALS(asm_simp_tac (!simpset addsimps [comp_refl])));
qed "lift_rec_preserve_comp";
goal Substitution.thy
- "!!n.u2 ~ v2 ==> ALL m:nat.ALL u1:redexes.ALL v1:redexes.\
+ "!!n. u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\
\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
by (etac Scomp.induct 1);
by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps
@@ -277,14 +277,14 @@
qed "subst_rec_preserve_comp";
goal Substitution.thy
- "!!n.regular(u) ==> ALL m:nat.regular(lift_rec(u,m))";
+ "!!n. regular(u) ==> ALL m:nat. regular(lift_rec(u,m))";
by (eresolve_tac [Sreg.induct] 1);
by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset))));
qed "lift_rec_preserve_reg";
goal Substitution.thy
- "!!n.regular(v) ==> \
-\ ALL m:nat.ALL u:redexes.regular(u)-->regular(subst_rec(u,v,m))";
+ "!!n. regular(v) ==> \
+\ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))";
by (eresolve_tac [Sreg.induct] 1);
by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps
[lift_rec_preserve_reg])));
--- a/src/ZF/Resid/Substitution.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Substitution.thy Fri Oct 10 18:23:31 1997 +0200
@@ -18,9 +18,9 @@
defs
lift_rec_def "lift_rec(r,kg) ==
- redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))),
- %x m.(lam k:nat.Fun(m`(succ(k)))),
- %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
+ redex_rec(r,%i.(lam k:nat. if(i<k,Var(i),Var(succ(i)))),
+ %x m.(lam k:nat. Fun(m`(succ(k)))),
+ %b x y m p. lam k:nat. App(b,m`k,p`k))`kg"
(* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
@@ -32,12 +32,12 @@
*)
subst_rec_def "subst_rec(u,t,kg) ==
redex_rec(t,
- %i.(lam r:redexes.lam k:nat.
+ %i.(lam r:redexes. lam k:nat.
if(k<i,Var(i#-1),
if(k=i,r,Var(i)))),
- %x m.(lam r:redexes.lam k:nat.
+ %x m.(lam r:redexes. lam k:nat.
Fun(m`(lift(r))`(succ(k)))),
- %b x y m p.lam r:redexes.lam k:nat.
+ %b x y m p. lam r:redexes. lam k:nat.
App(b,m`r`k,p`r`k))`u`kg"
--- a/src/ZF/Resid/Terms.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Terms.ML Fri Oct 10 18:23:31 1997 +0200
@@ -42,13 +42,13 @@
(* ------------------------------------------------------------------------- *)
goalw Terms.thy [unmark_def]
- "!!u.u:redexes ==> unmark(u):lambda";
+ "!!u. u:redexes ==> unmark(u):lambda";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS Asm_simp_tac);
qed "unmark_type";
goal Terms.thy
- "!!u.u:lambda ==> unmark(u) = u";
+ "!!u. u:lambda ==> unmark(u) = u";
by (eresolve_tac [lambda.induct] 1);
by (ALLGOALS Asm_simp_tac);
qed "lambda_unmark";
@@ -59,14 +59,14 @@
(* ------------------------------------------------------------------------- *)
goal Terms.thy
- "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda";
+ "!!u.[|v:lambda|]==> ALL k:nat. lift_rec(v,k):lambda";
by (eresolve_tac [lambda.induct] 1);
by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset))));
qed "liftL_typea";
val liftL_type =liftL_typea RS bspec ;
goal Terms.thy
- "!!n.[|v:lambda|]==> ALL n:nat.ALL u:lambda.subst_rec(u,v,n):lambda";
+ "!!n.[|v:lambda|]==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
by (eresolve_tac [lambda.induct] 1);
by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [liftL_type])));
qed "substL_typea";
--- a/src/ZF/Resid/Terms.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Terms.thy Fri Oct 10 18:23:31 1997 +0200
@@ -24,9 +24,9 @@
type_intrs "redexes.intrs@bool_typechecks"
defs
- unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
- %x m.Fun(m),
- %b x y m p.Apl(m,p))"
+ unmark_def "unmark(u) == redex_rec(u,%i. Var(i),
+ %x m. Fun(m),
+ %b x y m p. Apl(m,p))"
end
--- a/src/ZF/Sum.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Sum.ML Fri Oct 10 18:23:31 1997 +0200
@@ -200,11 +200,11 @@
by (etac CollectD1 1);
qed "PartD1";
-goal Sum.thy "Part(A,%x.x) = A";
+goal Sum.thy "Part(A,%x. x) = A";
by (Blast_tac 1);
qed "Part_id";
-goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
+goal Sum.thy "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}";
by (Blast_tac 1);
qed "Part_Inr2";
--- a/src/ZF/WF.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/WF.thy Fri Oct 10 18:23:31 1997 +0200
@@ -26,7 +26,7 @@
is_recfun_def "is_recfun(r,a,H,f) ==
(f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
- the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
+ the_recfun_def "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"
wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
--- a/src/ZF/ZF.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ZF.ML Fri Oct 10 18:23:31 1997 +0200
@@ -53,7 +53,7 @@
val ball_tac = dtac bspec THEN' assume_tac;
(*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
-qed_goal "ball_triv" ZF.thy "(ALL x:A.P) <-> ((EX x. x:A) --> P)"
+qed_goal "ball_triv" ZF.thy "(ALL x:A. P) <-> ((EX x. x:A) --> P)"
(fn _=> [ simp_tac (!simpset addsimps [Ball_def]) 1 ]);
Addsimps [ball_triv];
@@ -70,7 +70,7 @@
(*Not of the general form for such rules; ~EX has become ALL~ *)
qed_goal "bexCI" ZF.thy
- "[| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A.P(x)"
+ "[| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A. P(x)"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
@@ -86,7 +86,7 @@
AddSEs [bexE];
(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
-qed_goal "bex_triv" ZF.thy "(EX x:A.P) <-> ((EX x. x:A) & P)"
+qed_goal "bex_triv" ZF.thy "(EX x:A. P) <-> ((EX x. x:A) & P)"
(fn _=> [ simp_tac (!simpset addsimps [Bex_def]) 1 ]);
Addsimps [bex_triv];
@@ -101,7 +101,7 @@
(*** Rules for subsets ***)
qed_goalw "subsetI" ZF.thy [subset_def]
- "(!!x.x:A ==> x:B) ==> A <= B"
+ "(!!x. x:A ==> x:B) ==> A <= B"
(fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
(*Rule in Modus Ponens style [was called subsetE] *)
@@ -271,7 +271,7 @@
"b : {f(x). x:A} <-> (EX x:A. b=f(x))"
(fn _ => [Blast_tac 1]);
-goal ZF.thy "{x.x:A} = A";
+goal ZF.thy "{x. x:A} = A";
by (Blast_tac 1);
qed "triv_RepFun";
@@ -344,7 +344,7 @@
(REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
qed_goal "UN_cong" ZF.thy
- "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A.C(x)) = (UN x:B.D(x))"
+ "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A. C(x)) = (UN x:B. D(x))"
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
(*No "Addcongs [UN_cong]" because UN is a combination of constants*)
@@ -404,7 +404,7 @@
(rtac (minor RS RepFunI) 1) ]);
qed_goal "INT_cong" ZF.thy
- "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A.C(x)) = (INT x:B.D(x))"
+ "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))"
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
(*No "Addcongs [INT_cong]" because INT is a combination of constants*)
--- a/src/ZF/ZF.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ZF.thy Fri Oct 10 18:23:31 1997 +0200
@@ -129,7 +129,7 @@
"<x, y, z>" == "<x, <y, z>>"
"<x, y>" == "Pair(x, y)"
"%<x,y,zs>.b" == "split(%x <y,zs>.b)"
- "%<x,y>.b" == "split(%x y.b)"
+ "%<x,y>.b" == "split(%x y. b)"
syntax (symbols)
@@ -190,7 +190,7 @@
The resulting set (for functional P) is the same as with
PrimReplace, but the rules are simpler. *)
- Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))"
+ Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
(* Functional form of replacement -- analgous to ML's map functional *)
@@ -246,7 +246,7 @@
Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
(* Restrict the function f to the domain A *)
- restrict_def "restrict(f,A) == lam x:A.f`x"
+ restrict_def "restrict(f,A) == lam x:A. f`x"
end
--- a/src/ZF/ex/BT.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/BT.thy Fri Oct 10 18:23:31 1997 +0200
@@ -20,7 +20,7 @@
defs
bt_rec_def
- "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
+ "bt_rec(t,c,h) == Vrec(t, %t g. bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
n_nodes_def "n_nodes(t) == bt_rec(t, 0, %x y z r s. succ(r#+s))"
n_leaves_def "n_leaves(t) == bt_rec(t, succ(0), %x y z r s. r#+s)"
--- a/src/ZF/ex/Brouwer.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Brouwer.ML Fri Oct 10 18:23:31 1997 +0200
@@ -56,7 +56,7 @@
(*In fact it's isomorphic to nat, but we need a recursion operator for
Well to prove this.*)
-goal Brouwer.thy "Well(bool, %x.x) = 1 + (1 -> Well(bool, %x.x))";
+goal Brouwer.thy "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))";
by (resolve_tac [Well_unfold RS trans] 1);
by (simp_tac (!simpset addsimps [Sigma_bool, Pi_empty1, succ_def]) 1);
qed "Well_bool_unfold";
--- a/src/ZF/ex/Limit.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Limit.ML Fri Oct 10 18:23:31 1997 +0200
@@ -150,7 +150,7 @@
qed "isubI";
val prems = goalw Limit.thy [isub_def] (* isubE *)
- "!!z.[|isub(D,X,x);[|x:set(D); !!n.n:nat==>rel(D,X`n,x)|] ==> P|] ==> P";
+ "!!z.[|isub(D,X,x);[|x:set(D); !!n. n:nat==>rel(D,X`n,x)|] ==> P|] ==> P";
by (safe_tac (!claset));
by (Asm_simp_tac 1);
qed "isubE";
@@ -248,7 +248,7 @@
(*----------------------------------------------------------------------*)
val prems = goalw Limit.thy [pcpo_def] (* pcpoI *)
- "[|!!y.y:set(D)==>rel(D,x,y); x:set(D); cpo(D)|]==>pcpo(D)";
+ "[|!!y. y:set(D)==>rel(D,x,y); x:set(D); cpo(D)|]==>pcpo(D)";
by (rtac conjI 1);
by (resolve_tac prems 1);
by (rtac bexI 1);
@@ -322,7 +322,7 @@
qed "islub_const";
val prems = goal Limit.thy (* lub_const *)
- "[|x:set(D); cpo(D)|] ==> lub(D,lam n:nat.x) = x";
+ "[|x:set(D); cpo(D)|] ==> lub(D,lam n:nat. x) = x";
by (rtac islub_unique 1);
by (rtac cpo_lub 1);
by (rtac chain_const 1);
@@ -512,7 +512,7 @@
qed "matrix_chain_right";
val prems = goalw Limit.thy [matrix_def] (* matrix_chainI *)
- "[|!!x.x:nat==>chain(D,M`x); !!y.y:nat==>chain(D,lam x:nat. M`x`y); \
+ "[|!!x. x:nat==>chain(D,M`x); !!y. y:nat==>chain(D,lam x:nat. M`x`y); \
\ M:nat->nat->set(D); cpo(D)|] ==> matrix(D,M)";
by (safe_tac (!claset addSIs [ballI]));
by (cut_inst_tac[("y1","m"),("n","n")](hd(tl prems) RS chain_rel) 2);
@@ -529,7 +529,7 @@
(fn prems => [Asm_full_simp_tac 1]);
val lemma2 = prove_goal Limit.thy
- "!!z.[|x:nat; m:nat; rel(D,(lam n:nat.M`n`m1)`x,(lam n:nat.M`n`m1)`m)|] ==> \
+ "!!z.[|x:nat; m:nat; rel(D,(lam n:nat. M`n`m1)`x,(lam n:nat. M`n`m1)`m)|] ==> \
\ rel(D,M`x`m1,M`m`m1)"
(fn prems => [Asm_full_simp_tac 1]);
@@ -574,7 +574,7 @@
qed "isub_lemma";
val prems = goalw Limit.thy [chain_def] (* matrix_chain_lub *)
- "[|matrix(D,M); cpo(D)|] ==> chain(D,lam n:nat.lub(D,lam m:nat.M`n`m))";
+ "[|matrix(D,M); cpo(D)|] ==> chain(D,lam n:nat. lub(D,lam m:nat. M`n`m))";
by (safe_tac (!claset));
by (rtac lam_type 1);
by (rtac islub_in 1);
@@ -1335,7 +1335,7 @@
val prems = goalw Limit.thy [chain_def] (* chain_iprod *)
"[|chain(iprod(DD),X); !!n. n:nat ==> cpo(DD`n); n:nat|] ==> \
-\ chain(DD`n,lam m:nat.X`m`n)";
+\ chain(DD`n,lam m:nat. X`m`n)";
by (safe_tac (!claset));
by (rtac lam_type 1);
by (rtac apply_type 1);
@@ -1350,7 +1350,7 @@
val prems = goalw Limit.thy [islub_def,isub_def] (* islub_iprod *)
"[|chain(iprod(DD),X); !!n. n:nat ==> cpo(DD`n)|] ==> \
-\ islub(iprod(DD),X,lam n:nat. lub(DD`n,lam m:nat.X`m`n))";
+\ islub(iprod(DD),X,lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
by (safe_tac (!claset));
by (rtac iprodI 1);
by (rtac lam_type 1);
@@ -1391,7 +1391,7 @@
val prems = goalw Limit.thy [islub_def,isub_def] (* lub_iprod *)
"[|chain(iprod(DD),X); !!n. n:nat ==> cpo(DD`n)|] ==> \
-\ lub(iprod(DD),X) = (lam n:nat. lub(DD`n,lam m:nat.X`m`n))";
+\ lub(iprod(DD),X) = (lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
brr((cpo_lub RS islub_unique)::islub_iprod::cpo_iprod::prems) 1;
qed "lub_iprod";
@@ -2758,7 +2758,7 @@
qed "suffix_lemma";
val mediatingI = prove_goalw Limit.thy [mediating_def]
- "[|emb(E,G,t); !!n.n:nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)"
+ "[|emb(E,G,t); !!n. n:nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)"
(fn prems => [safe_tac (!claset),trr prems 1]);
val mediating_emb = prove_goalw Limit.thy [mediating_def]
--- a/src/ZF/ex/ListN.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/ListN.thy Fri Oct 10 18:23:31 1997 +0200
@@ -16,5 +16,5 @@
intrs
NilI "<0,Nil> : listn(A)"
ConsI "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
- type_intrs "nat_typechecks @ list.intrs"
+ type_intrs "nat_typechecks @ list. intrs"
end
--- a/src/ZF/ex/Primrec.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Primrec.ML Fri Oct 10 18:23:31 1997 +0200
@@ -137,7 +137,7 @@
(*PROPERTY A 5', monotonicity for le *)
goal Primrec.thy
"!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)";
-by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
+by (res_inst_tac [("f", "%j. ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
qed "ack_le_mono2";
@@ -170,7 +170,7 @@
(*PROPERTY A 7', monotonicity for le *)
goal Primrec.thy
"!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
-by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
+by (res_inst_tac [("f", "%j. ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
qed "ack_le_mono1";
--- a/src/ZF/ex/Primrec.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Primrec.thy Fri Oct 10 18:23:31 1997 +0200
@@ -30,11 +30,11 @@
defs
- SC_def "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
+ SC_def "SC == lam l:list(nat).list_case(0, %x xs. succ(x), l)"
CONST_def "CONST(k) == lam l:list(nat).k"
- PROJ_def "PROJ(i) == lam l:list(nat). list_case(0, %x xs.x, drop(i,l))"
+ PROJ_def "PROJ(i) == lam l:list(nat). list_case(0, %x xs. x, drop(i,l))"
COMP_def "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
@@ -57,7 +57,7 @@
PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
monos "[list_mono]"
con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
- type_intrs "nat_typechecks @ list.intrs @
+ type_intrs "nat_typechecks @ list. intrs @
[lam_type, list_case_type, drop_type, map_type,
apply_type, rec_type]"
--- a/src/ZF/ex/PropLog.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/PropLog.thy Fri Oct 10 18:23:31 1997 +0200
@@ -48,7 +48,7 @@
prop_rec_def
"prop_rec(p,b,c,h) ==
- Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
+ Vrec(p, %p g. prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
(** Semantics of propositional logic **)
is_true_def
--- a/src/ZF/ex/Rmap.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Rmap.thy Fri Oct 10 18:23:31 1997 +0200
@@ -19,7 +19,7 @@
ConsI "[| <x,y>: r; <xs,ys> : rmap(r) |] ==>
<Cons(x,xs), Cons(y,ys)> : rmap(r)"
- type_intrs "[domainI,rangeI] @ list.intrs"
+ type_intrs "[domainI,rangeI] @ list. intrs"
end
--- a/src/ZF/ex/TF.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/TF.ML Fri Oct 10 18:23:31 1997 +0200
@@ -229,13 +229,13 @@
(** theorems about TF_map **)
-goal TF.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
+goal TF.thy "!!z A. z: tree_forest(A) ==> TF_map(%u. u, z) = z";
by (etac tree_forest.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "TF_map_ident";
goal TF.thy
- "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
+ "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u. h(j(u)), z)";
by (etac tree_forest.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "TF_map_compose";
--- a/src/ZF/ex/TF.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/TF.thy Fri Oct 10 18:23:31 1997 +0200
@@ -37,13 +37,13 @@
"TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))"
TF_map_def
- "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil,
+ "TF_map(h,z) == TF_rec(z, %x f r. Tcons(h(x),r), Fnil,
%t f r1 r2. Fcons(r1,r2))"
TF_size_def
- "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
+ "TF_size(z) == TF_rec(z, %x f r. succ(r), 0, %t f r1 r2. r1#+r2)"
TF_preorder_def
- "TF_preorder(z) == TF_rec(z, %x f r.Cons(x,r), Nil, %t f r1 r2. r1@r2)"
+ "TF_preorder(z) == TF_rec(z, %x f r. Cons(x,r), Nil, %t f r1 r2. r1@r2)"
end
--- a/src/ZF/ex/Term.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Term.ML Fri Oct 10 18:23:31 1997 +0200
@@ -105,7 +105,7 @@
val [rew,tslist] = goal Term.thy
"[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \
-\ j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))";
+\ j(Apply(a,ts)) = d(a, ts, map(%Z. j(Z), ts))";
by (rewtac rew);
by (rtac (tslist RS term_rec) 1);
qed "def_term_rec";
@@ -177,13 +177,13 @@
(** theorems about term_map **)
-goal Term.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
+goal Term.thy "!!t A. t: term(A) ==> term_map(%u. u, t) = t";
by (etac term_induct_eqn 1);
by (asm_simp_tac (!simpset addsimps [map_ident]) 1);
qed "term_map_ident";
goal Term.thy
- "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
+ "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
by (etac term_induct_eqn 1);
by (asm_simp_tac (!simpset addsimps [map_compose]) 1);
qed "term_map_compose";
--- a/src/ZF/ex/Term.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Term.thy Fri Oct 10 18:23:31 1997 +0200
@@ -29,7 +29,7 @@
defs
term_rec_def
"term_rec(t,d) ==
- Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
+ Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z. g`z, zs)), t))"
term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
--- a/src/ZF/func.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/func.ML Fri Oct 10 18:23:31 1997 +0200
@@ -164,15 +164,15 @@
qed "lamD";
val prems = goalw ZF.thy [lam_def, Pi_def, function_def]
- "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)";
+ "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";
by (blast_tac (!claset addIs prems) 1);
qed "lam_type";
-goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
+goal ZF.thy "(lam x:A. b(x)) : A -> {b(x). x:A}";
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
qed "lam_funtype";
-goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
+goal ZF.thy "!!a A. a : A ==> (lam x:A. b(x)) ` a = b(a)";
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
qed "beta";
@@ -230,7 +230,7 @@
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
val prems = goal ZF.thy
"[| f: Pi(A,B); \
-\ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A.b(x)) |] ==> P \
+\ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P \
\ |] ==> P";
by (resolve_tac prems 1);
by (rtac (eta RS sym) 2);
@@ -240,7 +240,7 @@
(** Images of functions **)
-goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
+goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
by (Blast_tac 1);
qed "image_lam";
--- a/src/ZF/mono.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/mono.ML Fri Oct 10 18:23:31 1997 +0200
@@ -178,13 +178,13 @@
qed "imp_refl";
val [PQimp] = goal IFOL.thy
- "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
+ "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
by IntPr.safe_tac;
by (etac (PQimp RS mp RS exI) 1);
qed "ex_mono";
val [PQimp] = goal IFOL.thy
- "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
+ "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
by IntPr.safe_tac;
by (etac (spec RS (PQimp RS mp)) 1);
qed "all_mono";
--- a/src/ZF/pair.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/pair.ML Fri Oct 10 18:23:31 1997 +0200
@@ -131,7 +131,7 @@
(*** Eliminator - split ***)
(*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "split" ZF.thy [split_def] "split(%x y.c(x,y), <a,b>) == c(a,b)"
+qed_goalw "split" ZF.thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
(fn _ => [ (Simp_tac 1),
(rtac reflexive_thm 1) ]);
@@ -140,7 +140,7 @@
qed_goal "split_type" ZF.thy
"[| p:Sigma(A,B); \
\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
-\ |] ==> split(%x y.c(x,y), p) : C(p)"
+\ |] ==> split(%x y. c(x,y), p) : C(p)"
(fn major::prems=>
[ (rtac (major RS SigmaE) 1),
(asm_simp_tac (!simpset addsimps prems) 1) ]);
--- a/src/ZF/simpdata.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/simpdata.ML Fri Oct 10 18:23:31 1997 +0200
@@ -20,8 +20,8 @@
"(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
"(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
"(ALL x:0.P(x)) <-> True",
- "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
- "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))",
+ "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
+ "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
"(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
"(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
"(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
@@ -33,8 +33,8 @@
["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
"(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
"(EX x:0.P(x)) <-> False",
- "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))",
- "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))",
+ "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
+ "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
"(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
"(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))",
"(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
--- a/src/ZF/subset.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/subset.ML Fri Oct 10 18:23:31 1997 +0200
@@ -77,15 +77,15 @@
qed "subset_UN_iff_eq";
qed_goal "UN_subset_iff" ZF.thy
- "(UN x:A.B(x)) <= C <-> (ALL x:A. B(x) <= C)"
+ "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
(fn _ => [ Blast_tac 1 ]);
qed_goal "UN_upper" ZF.thy
- "!!x A. x:A ==> B(x) <= (UN x:A.B(x))"
+ "!!x A. x:A ==> B(x) <= (UN x:A. B(x))"
(fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
qed_goal "UN_least" ZF.thy
- "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A.B(x)) <= C"
+ "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
(fn [prem]=>
[ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -109,11 +109,11 @@
(*** Intersection of a family of sets ***)
qed_goal "INT_lower" ZF.thy
- "!!x. x:A ==> (INT x:A.B(x)) <= B(x)"
+ "!!x. x:A ==> (INT x:A. B(x)) <= B(x)"
(fn _ => [ Blast_tac 1 ]);
qed_goal "INT_greatest" ZF.thy
- "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A.B(x))"
+ "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
(fn [nonempty,prem] =>
[ rtac (nonempty RS RepFunI RS Inter_greatest) 1,
REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]);
--- a/src/ZF/upair.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/upair.ML Fri Oct 10 18:23:31 1997 +0200
@@ -213,7 +213,7 @@
(*Easier to apply than theI: conclusion has only one occurrence of P*)
qed_goal "theI2" ZF.thy
- "[| EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))"
+ "[| EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"
(fn prems => [ resolve_tac prems 1,
rtac theI 1,
resolve_tac prems 1 ]);