src/HOL/Groebner_Basis.thy
changeset 64246 15d1ee6e847b
parent 61799 4cf66f21b764
child 64248 690eb1ae8bb0
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Oct 16 09:31:05 2016 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Oct 16 09:31:06 2016 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  declare mod_mod_trivial[algebra]
     1.5  declare div_by_0[algebra]
     1.6  declare mod_by_0[algebra]
     1.7 -declare zmod_zdiv_equality[symmetric,algebra]
     1.8 +declare mult_div_mod_eq[algebra]
     1.9  declare div_mod_equality2[symmetric, algebra]
    1.10  declare div_minus_minus[algebra]
    1.11  declare mod_minus_minus[algebra]