From 092875d160a2d18c94bde41c6472e8031ab57313 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 17 Apr 2021 17:41:06 +0100
Subject: Patch proof. Now works on Isabelle2021.

---
 hott/Identity.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'hott')

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
 
-- 
cgit v1.2.3