src/HOL/Groebner_Basis.thy

 declare mod_minus_right[algebra]
 declare div_0[algebra]
 declare mod_0[algebra]
 declare mod_by_1[algebra]
 declare div_by_1[algebra]
-declare zmod_minus1_right[algebra]
-declare zdiv_minus1_right[algebra]
+declare mod_minus1_right[algebra]
+declare div_minus1_right[algebra]
 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
 declare mod_mult_self2_is_0[algebra]
 declare mod_mult_self1_is_0[algebra]
 declare zmod_eq_0_iff[algebra]