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.
generalize syntax of SPASS proofs
authorblanchet
Wed, 20 Feb 2013 17:31:28 +0100
changeset 51211 e5ef7a18f4a3
parent 51210 ec16ec9ab8d5
child 51212 2bbcc9cc12b4
generalize syntax of SPASS proofs
src/HOL/Tools/ATP/atp_proof.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 20 17:15:06 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 20 17:31:28 2013 +0100
@@ -460,8 +460,9 @@
 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
            derived from formulae <ident>* *)
 fun parse_spass_line x =
-  (parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
-     -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]"
+  (parse_spass_debug |-- scan_general_id --| $$ "[" --|
+     Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id
+     -- parse_spass_annotations --| $$ "]"
      -- parse_horn_clause --| $$ "."
      -- Scan.option (Scan.this_string "derived from formulae "
                      |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
isabelle