1 files changed, 7 insertions, 6 deletions

diff --git a/Sum.thy b/Sum.thy
index bf7b829..1e6e6b0 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -57,12 +57,13 @@ lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
   where "A \<times> B \<equiv> \<Sum>_:A. B"
 
-lemma
-  Pair_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : A \<times> B"
-  proof
-    fix b B assume "b : B"
-    then show "B : U" ..
-  qed
+text "The nondependent pair needs its own separate introduction rule."
+
+lemma Pair_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : A \<times> B"
+proof
+  fix b B assume "b : B"
+  then show "B : U" ..
+qed
 
 
 end
\ No newline at end of file