src/HOL/Transfer.thy
changeset 51437 8739f8abbecb
parent 51112 da97167e03f7
child 51955 04d9381bebff
     1.1 --- a/src/HOL/Transfer.thy	Sat Mar 16 17:22:05 2013 +0100
     1.2 +++ b/src/HOL/Transfer.thy	Sat Mar 16 20:51:23 2013 +0100
     1.3 @@ -57,6 +57,9 @@
     1.4  definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
     1.5    where "is_equality R \<longleftrightarrow> R = (op =)"
     1.6  
     1.7 +lemma is_equality_eq: "is_equality (op =)"
     1.8 +  unfolding is_equality_def by simp
     1.9 +
    1.10  text {* Handling of meta-logic connectives *}
    1.11  
    1.12  definition transfer_forall where
    1.13 @@ -179,9 +182,6 @@
    1.14  
    1.15  subsection {* Properties of relators *}
    1.16  
    1.17 -lemma is_equality_eq [transfer_rule]: "is_equality (op =)"
    1.18 -  unfolding is_equality_def by simp
    1.19 -
    1.20  lemma right_total_eq [transfer_rule]: "right_total (op =)"
    1.21    unfolding right_total_def by simp
    1.22