# HG changeset patch
# User haftmann
# Date 1476618453 -7200
# Node ID f537616459e6f4d2ebb971b7e8586538971e294a
# Parent  15d1ee6e847beeccf9133eaab206e0aeeb9421d6
avoid effectively subsumed rules;
simplified fact reference

diff -r 15d1ee6e847b -r f537616459e6 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun Oct 16 09:31:06 2016 +0200
+++ b/src/HOL/Presburger.thy	Sun Oct 16 13:47:33 2016 +0200
@@ -410,7 +410,7 @@
   end
 \<close> "Cooper's algorithm for Presburger arithmetic"
 
-declare dvd_eq_mod_eq_0 [symmetric, presburger]
+declare mod_eq_0_iff_dvd [presburger]
 declare mod_by_Suc_0 [presburger] 
 declare mod_0 [presburger]
 declare mod_by_1 [presburger]
@@ -418,13 +418,11 @@
 declare div_by_0 [presburger]
 declare mod_by_0 [presburger]
 declare mod_div_trivial [presburger]
-declare div_mod_equality2 [presburger]
-declare div_mod_equality [presburger]
 declare mult_div_mod_eq [presburger]
 declare div_mult_mod_eq [presburger]
 declare mod_mult_self1 [presburger]
 declare mod_mult_self2 [presburger]
-declare mod2_Suc_Suc[presburger]
+declare mod2_Suc_Suc [presburger]
 declare not_mod_2_eq_0_eq_1 [presburger] 
 declare nat_zero_less_power_iff [presburger]