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.
allow (~) syntax in TPTP proofs for unapplied negation
authorblanchet
Mon, 25 Sep 2023 17:16:32 +0200
changeset 78694 5e995ceb7490
parent 78693 1c0576840bf4
child 78695 41273636a82a
allow (~) syntax in TPTP proofs for unapplied negation
src/HOL/Tools/ATP/atp_proof.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle