aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
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