src/HOL/Groebner_Basis.thy
changeset 47160 8ada79014cb2
parent 47159 978c00c20a59
child 47161 8a32c2294498
     1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:27:49 2012 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:34:04 2012 +0200
     1.3 @@ -62,8 +62,8 @@
     1.4  declare mod_0[algebra]
     1.5  declare mod_by_1[algebra]
     1.6  declare div_by_1[algebra]
     1.7 -declare zmod_minus1_right[algebra]
     1.8 -declare zdiv_minus1_right[algebra]
     1.9 +declare mod_minus1_right[algebra]
    1.10 +declare div_minus1_right[algebra]
    1.11  declare mod_div_trivial[algebra]
    1.12  declare mod_mod_trivial[algebra]
    1.13  declare mod_mult_self2_is_0[algebra]