1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:34:04 2012 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:34:36 2012 +0200
     1.3 @@ -64,8 +64,6 @@
     1.4  declare div_by_1[algebra]
     1.5  declare mod_minus1_right[algebra]
     1.6  declare div_minus1_right[algebra]
     1.7 -declare mod_div_trivial[algebra]
     1.8 -declare mod_mod_trivial[algebra]
     1.9  declare mod_mult_self2_is_0[algebra]
    1.10  declare mod_mult_self1_is_0[algebra]
    1.11  declare zmod_eq_0_iff[algebra]