src/HOL/NumberTheory/Fib.thy
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