--- a/src/CCL/genrec.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/genrec.ML Fri Oct 10 17:10:12 1997 +0200
@@ -30,7 +30,7 @@
val prems = goalw Wfd.thy [letrec2_def]
"[| a : A; b : B; \
\ !!p q g.[| p:A; q:B; \
-\ ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
+\ ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
\ h(p,q,g) : D(p,q) |] ==> \
\ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
by (rtac (SPLITB RS subst) 1);
@@ -42,14 +42,14 @@
eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
qed "letrec2T";
-goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
+goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)";
by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
qed "lemma";
val prems = goalw Wfd.thy [letrec3_def]
"[| a : A; b : B; c : C; \
\ !!p q r g.[| p:A; q:B; r:C; \
-\ ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
+\ ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
\ g(x,y,z) : D(x,y,z) |] ==>\
\ h(p,q,r,g) : D(p,q,r) |] ==> \
\ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)";
@@ -75,14 +75,14 @@
qed "rcallT";
val major::prems = goal Wfd.thy
- "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
+ "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
\ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \
\ g(a,b) : E";
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
qed "rcall2T";
val major::prems = goal Wfd.thy
- "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
+ "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
\ g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; \
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
\ g(a,b,c) : E";
@@ -116,7 +116,7 @@
qed "hyprcallT";
val prems = goal Wfd.thy
- "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
+ "[| g(a,b) = c; ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
\ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \
\ a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \
\ P";
@@ -128,7 +128,7 @@
val prems = goal Wfd.thy
"[| g(a,b,c) = d; \
-\ ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
+\ ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
\ [| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P; \
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
\ P";
@@ -149,13 +149,13 @@
qed "rmIH1";
val prems = goal Wfd.thy
- "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
+ "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
\ P";
by (REPEAT (ares_tac prems 1));
qed "rmIH2";
val prems = goal Wfd.thy
- "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
+ "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
\ P |] ==> \
\ P";
by (REPEAT (ares_tac prems 1));