--- a/src/HOL/Transfer.thy Sat Mar 16 17:22:05 2013 +0100
+++ b/src/HOL/Transfer.thy Sat Mar 16 20:51:23 2013 +0100
@@ -57,6 +57,9 @@
definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
where "is_equality R \<longleftrightarrow> R = (op =)"
+lemma is_equality_eq: "is_equality (op =)"
+ unfolding is_equality_def by simp
+
text {* Handling of meta-logic connectives *}
definition transfer_forall where
@@ -179,9 +182,6 @@
subsection {* Properties of relators *}
-lemma is_equality_eq [transfer_rule]: "is_equality (op =)"
- unfolding is_equality_def by simp
-
lemma right_total_eq [transfer_rule]: "right_total (op =)"
unfolding right_total_def by simp