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.
fixed metis_steps_total - was off by one
authorsmolkas
Thu, 14 Feb 2013 23:54:46 +0100
changeset 51132 f8dc1c94ef8b
parent 51131 7de262be1e95
child 51133 fb16c4276620
fixed metis_steps_total - was off by one
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Feb 14 23:54:46 2013 +0100
@@ -60,7 +60,7 @@
          | Prove (_, _, _, Case_Split (cases, _)) =>
            Integer.add (fold (Integer.add o metis_steps_total) cases 1)
          | Prove (_, _, _, Subblock subproof) =>
-           Integer.add (metis_steps_total subproof)
+           Integer.add (metis_steps_total subproof + 1)
          | _ => I) proof 0
 
 end
isabelle