# HG changeset patch # User blanchet # Date 1626100217 -7200 # Node ID b304285fd80012dd799366207314d40c532aa42b # Parent 96a05b8462f952029c8654044388dcd334d048f6 parse logical operators in the right order w.r.t. backtracking diff -r 96a05b8462f9 -r b304285fd800 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Jul 12 16:30:16 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jul 12 16:30:17 2021 +0200 @@ -476,8 +476,8 @@ | role_of_tptp_string _ = Unknown val tptp_binary_ops = - [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, - tptp_equal, tptp_not_equal, tptp_app] + [tptp_and, tptp_or, tptp_implies, tptp_iff, tptp_if, tptp_equal, tptp_not_equal, tptp_not_and, + tptp_not_or, tptp_not_iff, tptp_app] fun parse_one_in_list xs = foldl1 (op ||) (map Scan.this_string xs)