src/HOL/Groebner_Basis.thy
changeset 30031 bd786c37af84
parent 30027 ab40c5e007e0
child 30034 60f64f112174
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 21:29:34 2009 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Feb 20 23:46:03 2009 +0100
     1.3 @@ -448,8 +448,8 @@
     1.4  declare zmod_zminus2[algebra]
     1.5  declare zdiv_zero[algebra]
     1.6  declare zmod_zero[algebra]
     1.7 -declare zmod_1[algebra]
     1.8 -declare zdiv_1[algebra]
     1.9 +declare mod_by_1[algebra]
    1.10 +declare div_by_1[algebra]
    1.11  declare zmod_minus1_right[algebra]
    1.12  declare zdiv_minus1_right[algebra]
    1.13  declare mod_div_trivial[algebra]