aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorJosh Chen2020-05-25 16:27:53 +0200
committerJosh Chen2020-05-25 16:27:53 +0200
commit22c5b895a4a2ba0ecb97a5c7ccab4b13c42c24e3 (patch)
treeb0e9ee79d4b7f373bb9cfb38b23c36d37318afb1 /hott
parent2f63e165d696688f0fcc721289889a8baa00cc02 (diff)
minor
Diffstat (limited to '')
-rw-r--r--hott/Nat.thy2
1 files changed, 1 insertions, 1 deletions
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