Refactor HoTT_Methods.thy, proved more stuff with new methods.

1 files changed, 4 insertions, 4 deletions

diff --git a/Sum.thy b/Sum.thy
index 7e688a2..bf7b829 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -59,10 +59,10 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
 
 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
+  proof
+    fix b B assume "b : B"
+    then show "B : U" ..
+  qed
 
 
 end
\ No newline at end of file