diff -r e76e77e0d615 -r 0ca998e83447 src/HOL/NumberTheory/Fib.thy --- a/src/HOL/NumberTheory/Fib.thy Mon Jul 31 20:56:49 2006 +0200 +++ b/src/HOL/NumberTheory/Fib.thy Mon Jul 31 21:06:40 2006 +0200 @@ -72,7 +72,6 @@ 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