simplified fact references
authorhaftmann
Sun Oct 16 13:47:35 2016 +0200 (2016-10-16)
changeset 64248690eb1ae8bb0
parent 64247 f537616459e6
child 64249 a3f654f9a46c
simplified fact references
src/HOL/Groebner_Basis.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Oct 16 13:47:33 2016 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Oct 16 13:47:35 2016 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  \<close> "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
     1.5  
     1.6  declare dvd_def[algebra]
     1.7 -declare dvd_eq_mod_eq_0[symmetric, algebra]
     1.8 +declare mod_eq_0_iff_dvd[algebra]
     1.9  declare mod_div_trivial[algebra]
    1.10  declare mod_mod_trivial[algebra]
    1.11  declare div_by_0[algebra]