diff options
author | Josh Chen | 2018-07-06 10:48:41 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-06 10:48:41 +0200 |
commit | 76deb7ae15fa00b5498ab43db020a0364499251e (patch) | |
tree | 706d25614154cf3767e1ad9e905a6074b620809a /Equal.thy | |
parent | b65450369f992171f166a53e9cab408819cd987f (diff) |
Added attributes to type elimination rules, not sure if these will actually be needed or useful later. Added [comp] attribute to be used by simplification met methods.
Diffstat (limited to 'Equal.thy')
-rw-r--r-- | Equal.thy | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -53,7 +53,9 @@ 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_elims [dest] = Equal_elim lemmas Equal_form_conds [elim, wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 +lemmas Equal_comps [comp] = Equal_comp end
\ No newline at end of file |