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.
parse more liberal MaSh suggestion syntax (for the eval driver)
authorblanchet
Thu, 06 Dec 2012 15:54:17 +0100
changeset 50401 8e5d7ef3da76
parent 50400 fe9223fdd060
child 50402 923f1e199f4f
parse more liberal MaSh suggestion syntax (for the eval driver)
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:42:23 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 15:54:17 2012 +0100
@@ -199,7 +199,8 @@
 fun extract_suggestion sugg =
   case space_explode "=" sugg of
     [name, weight] =>
-    SOME (unescape_meta name, Real.fromString weight |> the_default 0.0)
+    SOME (unescape_meta name, Real.fromString weight |> the_default 1.0)
+  | [name] => SOME (unescape_meta name, 1.0)
   | _ => NONE
 
 fun extract_query line =
isabelle