| changeset 64249 | a3f654f9a46c |
| parent 64248 | 690eb1ae8bb0 |
| child 64593 | 50c715579715 |
--- a/src/HOL/Groebner_Basis.thy Sun Oct 16 13:47:35 2016 +0200 +++ b/src/HOL/Groebner_Basis.thy Sun Oct 16 13:47:36 2016 +0200 @@ -57,7 +57,6 @@ 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]