From 76a009527d42c9939575f429a406a084c48fe653 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 23 Feb 2019 18:58:20 +0100
Subject: touchups

---
 Projections.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Projections.thy')

diff --git a/Projections.thy b/Projections.thy
index 8ff6b30..1473e08 100644
--- a/Projections.thy
+++ b/Projections.thy
@@ -21,7 +21,7 @@ declare fst_type [intro]
 
 lemma fst_cmp:
   assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "fst A <a, b> \<equiv> a"
-unfolding fst_def by compute (derive lems: assms)
+unfolding fst_def by (subst comp) (derive lems: assms)
 
 declare fst_cmp [comp]
 
-- 
cgit v1.2.3