src/HOL/ex/PER.thy
changeset 28616 ac1da69fbc5a
parent 23373 ead82c82da9e
child 35315 fbdc860d87a3
     1.1 --- a/src/HOL/ex/PER.thy	Thu Oct 16 22:44:24 2008 +0200
     1.2 +++ b/src/HOL/ex/PER.thy	Thu Oct 16 22:44:25 2008 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4  qed
     1.5  
     1.6  lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
     1.7 -  using eqv_class_eqI eqv_class_eqD' by blast
     1.8 +  using eqv_class_eqI eqv_class_eqD' by (blast del: eqv_refl)
     1.9  
    1.10  lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
    1.11    using eqv_class_eqI eqv_class_eqD by blast