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.
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
authorblanchet
Thu, 29 Apr 2010 17:31:08 +0200
changeset 36562 c6c2661bf08e
parent 36561 f91c71982811
child 36563 bba1e5f2b643
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 13:41:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 17:31:08 2010 +0200
@@ -186,7 +186,7 @@
 (* It is not clear why some literals are followed by sequences of stars. We
    ignore them. *)
 fun parse_starred_predicate_term pool =
-  parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ")
+  parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
 
 fun parse_horn_clause pool =
   Scan.repeat (parse_starred_predicate_term pool) --| $$ "|" --| $$ "|"
isabelle