src/HOL/Groebner_Basis.thy
changeset 64593 50c715579715
parent 64249 a3f654f9a46c
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sat Dec 17 15:22:14 2016 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4  declare zmod_eq_0_iff[algebra]
     1.5  declare dvd_0_left_iff[algebra]
     1.6  declare zdvd1_eq[algebra]
     1.7 -declare zmod_eq_dvd_iff[algebra]
     1.8 +declare mod_eq_dvd_iff[algebra]
     1.9  declare nat_mod_eq_iff[algebra]
    1.10  
    1.11  context semiring_parity