| changeset 30031 | bd786c37af84 |
| parent 30027 | ab40c5e007e0 |
| child 30034 | 60f64f112174 |
--- a/src/HOL/Groebner_Basis.thy Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/Groebner_Basis.thy Fri Feb 20 23:46:03 2009 +0100 @@ -448,8 +448,8 @@ declare zmod_zminus2[algebra] declare zdiv_zero[algebra] declare zmod_zero[algebra] -declare zmod_1[algebra] -declare zdiv_1[algebra] +declare mod_by_1[algebra] +declare div_by_1[algebra] declare zmod_minus1_right[algebra] declare zdiv_minus1_right[algebra] declare mod_div_trivial[algebra]