aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to 'hott')
-rw-r--r--hott/Identity.thy4
-rw-r--r--hott/Nat.thy2
2 files changed, 3 insertions, 3 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 8675134..308e664 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -473,7 +473,7 @@ Lemma (derive) right_whisker:
have "t \<bullet> refl x = t" by (rule pathcomp_refl)
also have ".. = s" by fact
also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric])
- finally show "t \<bullet> refl x = s \<bullet> refl x" by this
+ finally show "{}" by this
qed
done
@@ -486,7 +486,7 @@ Lemma (derive) left_whisker:
have "refl x \<bullet> t = t" by (rule refl_pathcomp)
also have ".. = s" by fact
also have ".. = refl x \<bullet> s" by (rule refl_pathcomp[symmetric])
- finally show "refl x \<bullet> t = refl x \<bullet> s" by this
+ finally show "{}" by this
qed
done
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