src/HOL/Tools/ATP/atp_problem.ML
changeset 77427 4cdefee3f97f
parent 76301 73b120e0dbfe
child 78788 5a14f2cc1ea0
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -64,6 +64,7 @@
 
   val tptp_cnf : string
   val tptp_fof : string
+  val tptp_tcf : string
   val tptp_tff : string
   val tptp_thf : string
   val tptp_has_type : string
@@ -222,6 +223,7 @@
 (* official TPTP syntax *)
 val tptp_cnf = "cnf"
 val tptp_fof = "fof"
+val tptp_tcf = "tcf" (* sometimes appears in E's output *)
 val tptp_tff = "tff"
 val tptp_thf = "thf"
 val tptp_has_type = ":"