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