2 files changed, 8 insertions, 7 deletions
diff --git a/Prod.thy b/Prod.thy
index 18582a8..7155a10 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -64,7 +64,7 @@ lemmas Prod_form_conds [elim, wellform] = Prod_form_cond1 Prod_form_cond2
 text "Nondependent functions are a special case."
 
 abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 40)
-  where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"  
+  where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"
 
 
 end
 \ No newline at end of file
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