# HG changeset patch
# User haftmann
# Date 1476618455 -7200
# Node ID 690eb1ae8bb0eb17cb6cd42670ae6e2561f20939
# Parent  f537616459e6f4d2ebb971b7e8586538971e294a
simplified fact references

diff -r f537616459e6 -r 690eb1ae8bb0 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Oct 16 13:47:33 2016 +0200
+++ b/src/HOL/Groebner_Basis.thy	Sun Oct 16 13:47:35 2016 +0200
@@ -51,7 +51,7 @@
 \<close> "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
 
 declare dvd_def[algebra]
-declare dvd_eq_mod_eq_0[symmetric, algebra]
+declare mod_eq_0_iff_dvd[algebra]
 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
 declare div_by_0[algebra]