# HG changeset patch
# User haftmann
# Date 1476618456 -7200
# Node ID a3f654f9a46c8521d7fd78c9f128bbc66aa20cd5
# Parent  690eb1ae8bb0eb17cb6cd42670ae6e2561f20939
dropped potentially explosive rule for groebner simpset, with no observable effect on examples

diff -r 690eb1ae8bb0 -r a3f654f9a46c src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Oct 16 13:47:35 2016 +0200
+++ b/src/HOL/Groebner_Basis.thy	Sun Oct 16 13:47:36 2016 +0200
@@ -57,7 +57,6 @@
 declare div_by_0[algebra]
 declare mod_by_0[algebra]
 declare mult_div_mod_eq[algebra]
-declare div_mod_equality2[symmetric, algebra]
 declare div_minus_minus[algebra]
 declare mod_minus_minus[algebra]
 declare div_minus_right[algebra]