| changeset 20272 | 0ca998e83447 |
| parent 18156 | 5a971b272f78 |
| child 20432 | 07ec57376051 |
--- 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