| changeset 30198 | 922f944f03b2 |
| parent 30042 | 31039ee583fa |
| child 30242 | aea5d7fa7ef5 |
--- a/src/HOL/Word/Num_Lemmas.thy Mon Mar 02 08:26:03 2009 +0100 +++ b/src/HOL/Word/Num_Lemmas.thy Mon Mar 02 16:53:55 2009 +0100 @@ -260,7 +260,7 @@ (** Rep_Integ **) lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}" - unfolding equiv_def refl_def quotient_def Image_def by auto + unfolding equiv_def refl_on_def quotient_def Image_def by auto lemmas Rep_Integ_ne = Integ.Rep_Integ [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]