From b65450369f992171f166a53e9cab408819cd987f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 4 Jul 2018 10:50:52 +0200
Subject: Trivial changes

---
 Prod.thy |  2 +-
 Sum.thy  | 13 +++++++------
 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
-- 
cgit v1.2.3