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