| changeset 64246 | 15d1ee6e847b |
| parent 61799 | 4cf66f21b764 |
| child 64248 | 690eb1ae8bb0 |
--- a/src/HOL/Groebner_Basis.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Groebner_Basis.thy Sun Oct 16 09:31:06 2016 +0200 @@ -56,7 +56,7 @@ declare mod_mod_trivial[algebra] declare div_by_0[algebra] declare mod_by_0[algebra] -declare zmod_zdiv_equality[symmetric,algebra] +declare mult_div_mod_eq[algebra] declare div_mod_equality2[symmetric, algebra] declare div_minus_minus[algebra] declare mod_minus_minus[algebra]