| changeset 64244 | e7102c40783c |
| parent 64242 | 93c6f0da5c70 |
| child 64246 | 15d1ee6e847b |
--- a/src/HOL/Presburger.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Presburger.thy Sun Oct 16 09:31:05 2016 +0200 @@ -411,7 +411,7 @@ \<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]