From 76deb7ae15fa00b5498ab43db020a0364499251e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 6 Jul 2018 10:48:41 +0200
Subject: 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.

---
 Equal.thy | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Equal.thy')

diff --git a/Equal.thy b/Equal.thy
index 51a69ae..cb4d4f1 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -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
-- 
cgit v1.2.3