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 parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y))
authorblanchet
Sun, 01 May 2011 18:37:24 +0200
changeset 42550 3031d342d514
parent 42549 b9754f26c7bc
child 42551 cd99d6d3027a
fixed parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y))
src/HOL/Tools/ATP/atp_proof.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
@@ -262,7 +262,7 @@
        >> (fn ((q, ts), phi) =>
               (* FIXME: TFF *)
               AQuant (q, map (rpair NONE o fo_term_head) ts, phi))
-    || $$ "~" |-- parse_formula >> mk_anot
+    || $$ "~" |-- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom) >> mk_anot
     || parse_atom)
    -- Scan.option ((Scan.this_string "=>" >> K AImplies
                     || Scan.this_string "<=>" >> K AIff
isabelle