Remove extra attributes for elimination rules, unneeded for now.

1 files changed, 1 insertions, 2 deletions

diff --git a/Equal.thy b/Equal.thy
index cb4d4f1..7732dd0 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -12,7 +12,7 @@ begin
 axiomatization
   Equal :: "[Term, Term, Term] \<Rightarrow> Term" and
   refl :: "Term \<Rightarrow> Term"  ("(refl'(_'))" 1000) and
-  indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term"  ("(indEqual[_])")
+  indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term"  ("(1indEqual[_])")
 
 
 section \<open>Syntax\<close>
@@ -53,7 +53,6 @@ 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