# HG changeset patch
# User blanchet
# Date 1695654992 -7200
# Node ID 5e995ceb7490b228ca4e577b69d9e414ab6aacfe
# Parent  1c0576840bf4072498231b4c9e58892da26f2537
allow (~) syntax in TPTP proofs for unapplied negation

diff -r 1c0576840bf4 -r 5e995ceb7490 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 25 17:16:32 2023 +0200
@@ -529,6 +529,7 @@
     >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), []))
   || parse_hol_quantifier >> mk_simple_aterm
   || $$ "(" |-- parse_hol_term --| $$ ")"
+  || Scan.this_string tptp_not >> mk_simple_aterm
   || parse_literal_binary_op >> mk_simple_aterm
   || parse_nonliteral_binary_op >> mk_simple_aterm) x
 and parse_applied_hol_term x =