src/HOL/NumberTheory/Fib.thy

--- 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