--- a/src/HOL/Transfer.thy Wed Oct 24 17:40:56 2012 +0200
+++ b/src/HOL/Transfer.thy Wed Oct 24 18:43:25 2012 +0200
@@ -52,6 +52,11 @@
definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
where "Rel r \<equiv> r"
+text {* Handling of equality relations *}
+
+definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+ where "is_equality R \<longleftrightarrow> R = (op =)"
+
text {* Handling of meta-logic connectives *}
definition transfer_forall where
@@ -98,6 +103,8 @@
ML_file "Tools/transfer.ML"
setup Transfer.setup
+declare refl [transfer_rule]
+
declare fun_rel_eq [relator_eq]
hide_const (open) Rel
@@ -172,6 +179,9 @@
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