From 45c3879db6850282bc067318e31cccf42e60ac8f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 26 Mar 2019 17:04:01 +0100
Subject: working towards biinv_imp_qinv

---
 HoTT_Methods.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index e45608e..0199a49 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -68,8 +68,8 @@ It also handles universes using @{method cumulativity}.
 The method @{method hierarchy} has been observed to cause looping in previous versions, and is hence no longer part of @{theory_text derive}.
 \<close>
 
-method derive uses lems declares comp =
-  (routine add: lems | compute add: lems comp: comp | cumulativity form: lems)+
+method derive uses lems unfold declares comp =
+  (unfold unfold | routine add: lems | compute add: lems comp: comp | cumulativity form: lems)+
 
 section \<open>Additional method combinators\<close>
 
-- 
cgit v1.2.3