src/HOL/Groebner_Basis.thy

 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
 declare div_by_0[algebra]
 declare mod_by_0[algebra]
 declare mult_div_mod_eq[algebra]
-declare div_mod_equality2[symmetric, algebra]
 declare div_minus_minus[algebra]
 declare mod_minus_minus[algebra]
 declare div_minus_right[algebra]
 declare mod_minus_right[algebra]
 declare div_0[algebra]