parse logical operators in the right order w.r.t. backtracking
authorblanchet
Mon, 12 Jul 2021 16:30:17 +0200
changeset 74234 b304285fd800
parent 74233 96a05b8462f9
child 74235 f0d231ead660
parse logical operators in the right order w.r.t. backtracking
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)