From 7823d59b2d9436f1bf0042fff62ee2bcc4c29ec0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 3 Jul 2018 18:57:57 +0200
Subject: Refactor HoTT_Methods.thy, proved more stuff with new methods.

---
 Sum.thy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Sum.thy')

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
-- 
cgit v1.2.3