src/HOL/Presburger.thy

       SIMPLE_METHOD' (Cooper.tac elim add_ths del_ths ctxt))
   end
 \<close> "Cooper's algorithm for Presburger arithmetic"
 
 declare dvd_eq_mod_eq_0 [symmetric, presburger]
-declare mod_1 [presburger] 
+declare mod_by_Suc_0 [presburger] 
 declare mod_0 [presburger]
 declare mod_by_1 [presburger]
 declare mod_self [presburger]
 declare div_by_0 [presburger]
 declare mod_by_0 [presburger]