diff options
| author | Josh Chen | 2019-03-01 20:44:02 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-03-01 20:44:02 +0100 |
| commit | fa413a91f73773c4cb9c83ed65837320b598e1d4 (patch) | |
| tree | 479dfb0e50e1a1667232aedb29a15787997c6cd1 /HoTT_Methods.thy | |
| parent | c33f290df52e646edcf0589d98bd89da8ce288ec (diff) | |
finished proof of transport_biinv
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Methods.thy | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index ad7384d..27f252b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -70,7 +70,6 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}. method derive uses lems declares comp = (routine add: lems | compute add: lems comp: comp | cumulativity form: lems | hierarchy)+ - section \<open>Additional method combinators\<close> text \<open> |