aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorJosh Chen2021-04-17 17:41:06 +0100
committerJosh Chen2021-04-17 17:41:06 +0100
commit092875d160a2d18c94bde41c6472e8031ab57313 (patch)
tree94a8a08dcf264294fb6a128d1f32912c0d86f829 /hott
parent3a34ca2b43fbd5725a7435dfafdb4cf179a8ec8b (diff)
Patch proof. Now works on Isabelle2021.
Diffstat (limited to 'hott')
-rw-r--r--hott/Identity.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 0531b74..9ae0894 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -244,7 +244,7 @@ Lemma (def) ap_funcomp:
"p: x = y"
shows "(g \<circ> f)[p] = g[f[p]]"
apply (eq p)
- \<^item> by compute
+ \<^item> by (subst comp; typechk?)+
\<^item> by compute refl
done