From 22c5b895a4a2ba0ecb97a5c7ccab4b13c42c24e3 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 16:27:53 +0200
Subject: minor

---
 hott/Nat.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'hott')

diff --git a/hott/Nat.thy b/hott/Nat.thy
index 4825404..311f2d9 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -104,7 +104,7 @@ Lemma (derive) add_comm:
       proof reduce
         have "suc (m + n) = suc (n + m)" by (eq ih) intro
         also have "'' = n + suc m" by (rule add_suc[symmetric])
-        finally show "suc (m + n) = n + suc m" by this reduce
+        finally show "suc (m + n) = n + suc m" by this
       qed
   done
 
-- 
cgit v1.2.3