src/HOL/Groebner_Basis.thy
changeset 47159 978c00c20a59
parent 47142 d64fa2ca54b8
child 47160 8ada79014cb2
     1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 14:49:56 2012 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:27:49 2012 +0200
     1.3 @@ -54,10 +54,10 @@
     1.4  declare mod_by_0[algebra]
     1.5  declare zmod_zdiv_equality[symmetric,algebra]
     1.6  declare zdiv_zmod_equality[symmetric, algebra]
     1.7 -declare zdiv_zminus_zminus[algebra]
     1.8 -declare zmod_zminus_zminus[algebra]
     1.9 -declare zdiv_zminus2[algebra]
    1.10 -declare zmod_zminus2[algebra]
    1.11 +declare div_minus_minus[algebra]
    1.12 +declare mod_minus_minus[algebra]
    1.13 +declare div_minus_right[algebra]
    1.14 +declare mod_minus_right[algebra]
    1.15  declare div_0[algebra]
    1.16  declare mod_0[algebra]
    1.17  declare mod_by_1[algebra]