diff options
author | Josh Chen | 2018-07-03 18:57:57 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-03 18:57:57 +0200 |
commit | 7823d59b2d9436f1bf0042fff62ee2bcc4c29ec0 (patch) | |
tree | e45df70f36abdedfa0e5c2bcaebfb11022b18a41 /Equal.thy | |
parent | 9ffa5ed2a972db4ae6274a7852de37945a32ab0e (diff) |
Refactor HoTT_Methods.thy, proved more stuff with new methods.
Diffstat (limited to '')
-rw-r--r-- | Equal.thy | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -53,7 +53,7 @@ and \<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> f a" lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -lemmas Equal_form_conds [elim] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 +lemmas Equal_form_conds [elim, wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 end
\ No newline at end of file |