Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
a proof step corrected due to the changement in the presburger method.
authorchaieb
Fri, 11 Nov 2005 10:50:43 +0100
changeset 18156 5a971b272f78
parent 18155 e5ab63ca6b0f
child 18157 72e1956440ad
a proof step corrected due to the changement in the presburger method.
src/HOL/NumberTheory/Fib.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle