# HG changeset patch
# User chaieb
# Date 1131702643 -3600
# Node ID 5a971b272f7823742cfffba87b2d7dd1d0c49694
# Parent  e5ab63ca6b0f2f56bb97cfb580b14d0f25d838dc
a proof step corrected due to the changement in the presburger method.

diff -r e5ab63ca6b0f -r 5a971b272f78 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Fri Nov 11 10:49:59 2005 +0100
+++ b/src/HOL/NumberTheory/Fib.thy	Fri Nov 11 10:50:43 2005 +0100
@@ -72,7 +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
+  apply (presburger (no_abs))
   done
 
 text{*We now obtain a version for the natural numbers via the coercion