aboutsummaryrefslogtreecommitdiff
path: root/hott/Nat.thy
diff options
context:
space:
mode:
Diffstat (limited to 'hott/Nat.thy')
-rw-r--r--hott/Nat.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 22c1860..50b7996 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -151,7 +151,7 @@ Lemma (derive) zero_mul:
proof reduce
have "0 + 0 * n = 0 + 0 " by (eq ih) refl
also have ".. = 0" by reduce refl
- finally show "0 + 0 * n = 0" by this
+ finally show "{}" by this
qed
done