| changeset 47165 | 9344891b504b |
| parent 47161 | 8a32c2294498 |
| child 47432 | e1576d13e933 |
--- a/src/HOL/Groebner_Basis.thy Tue Mar 27 16:04:51 2012 +0200 +++ b/src/HOL/Groebner_Basis.thy Tue Mar 27 19:21:05 2012 +0200 @@ -53,7 +53,7 @@ declare div_by_0[algebra] declare mod_by_0[algebra] declare zmod_zdiv_equality[symmetric,algebra] -declare zdiv_zmod_equality[symmetric, algebra] +declare div_mod_equality2[symmetric, algebra] declare div_minus_minus[algebra] declare mod_minus_minus[algebra] declare div_minus_right[algebra]