aboutsummaryrefslogtreecommitdiff
path: root/Equal.thy
diff options
context:
space:
mode:
Diffstat (limited to 'Equal.thy')
-rw-r--r--Equal.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Equal.thy b/Equal.thy
index f0ced68..51a69ae 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -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