diff options
| author | Josh Chen | 2019-03-26 17:04:01 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-03-26 17:04:01 +0100 |
| commit | 45c3879db6850282bc067318e31cccf42e60ac8f (patch) | |
| tree | fd7753a339ee8a0e90bb97f80fc4105666ed7288 /HoTT_Methods.thy | |
| parent | 6dd1b27f7f84b17ad88e5b382042bd0c577a92f4 (diff) | |
working towards biinv_imp_qinv
Diffstat (limited to 'HoTT_Methods.thy')
| -rw-r--r-- | HoTT_Methods.thy | 4 |
1 files changed, 2 insertions, 2 deletions
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> |