changeset 20432 | 07ec57376051 |
parent 20272 | 0ca998e83447 |
child 23315 | df3a7e9ebadb |
--- a/src/HOL/NumberTheory/Fib.thy Tue Aug 29 21:43:34 2006 +0200 +++ b/src/HOL/NumberTheory/Fib.thy Wed Aug 30 03:19:08 2006 +0200 @@ -72,6 +72,7 @@ apply (simp add: fib.Suc_Suc mod_Suc) apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric]) + apply (presburger (no_abs)) done text{*We now obtain a version for the natural numbers via the coercion