# HG changeset patch
# User paulson
# Date 940252821 -7200
# Node ID 4547f0bd94545e1f62eadf32806b7efb7d80bc25
# Parent  43b03d412b82b1d886b71bd5f16d325606287073
fixed comments

diff -r 43b03d412b82 -r 4547f0bd9454 src/Provers/split_paired_all.ML
--- 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;