--- a/src/Provers/split_paired_all.ML Mon Oct 18 15:18:24 1999 +0200
+++ b/src/Provers/split_paired_all.ML Mon Oct 18 15:20:21 1999 +0200
@@ -44,15 +44,15 @@
(*lemma "P p == P (fst p, snd p)"*)
val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
- (*lemma "!!a b. PROP (a, b) ==> PROP P p"*)
+ (*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*)
val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p))
(fn prems => [resolve_tac prems 1]);
- (*lemma "!!a b. PROP (a, b) ==> !!x. PROP P x"*)
+ (*lemma "(!!a b. PROP P (a,b)) ==> !!x. PROP P x"*)
val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x))
(fn prems => [rtac lem2 1, resolve_tac prems 1]);
- (*lemma "!!x. PROP P x ==> !!a b. PROP (a, b)"*)
+ (*lemma "(!!x. PROP P x) ==> !!a b. PROP P (a,b)"*)
val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b))
(fn prems => [resolve_tac prems 1]);
in standard (Thm.equal_intr lem4 lem3) end;