| changeset 30042 | 31039ee583fa |
| parent 30034 | 60f64f112174 |
| child 30079 | 293b896b9c25 |
--- a/src/HOL/Groebner_Basis.thy Sat Feb 21 09:58:45 2009 +0100 +++ b/src/HOL/Groebner_Basis.thy Sat Feb 21 20:52:30 2009 +0100 @@ -457,7 +457,7 @@ declare mod_mult_self2_is_0[algebra] declare mod_mult_self1_is_0[algebra] declare zmod_eq_0_iff[algebra] -declare zdvd_0_left[algebra] +declare dvd_0_left_iff[algebra] declare zdvd1_eq[algebra] declare zmod_eq_dvd_iff[algebra] declare nat_mod_eq_iff[algebra]