| changeset 47161 | 8a32c2294498 |
| parent 47160 | 8ada79014cb2 |
| child 47165 | 9344891b504b |
--- a/src/HOL/Groebner_Basis.thy Tue Mar 27 15:34:04 2012 +0200 +++ b/src/HOL/Groebner_Basis.thy Tue Mar 27 15:34:36 2012 +0200 @@ -64,8 +64,6 @@ declare div_by_1[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]