# HG changeset patch
# User blanchet
# Date 1572008396 -7200
# Node ID 535ff1eac86c6a9922ef5e4876e1145143a34ced
# Parent  25c1ff13dbdbd877058ebacec8abdc7bb1dc8c9c
removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0

diff -r 25c1ff13dbdb -r 535ff1eac86c src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 14:55:14 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 14:59:56 2019 +0200
@@ -102,14 +102,14 @@
 historical.}
 %
 The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
-\cite{schulz-2002}, E-ToFoF \cite{tofof}, iProver \cite{korovin-2009}, LEO-II
-\cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK
-\cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire
-\cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and
-Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or
-remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The
-supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT
-\cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always run locally.
+\cite{schulz-2002}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III
+\cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
+\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002},
+Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. The
+ATPs are run either locally or remotely via the System\-On\-TPTP web service
+\cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4
+\cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are
+always run locally.
 
 The problem passed to the external provers (or solvers) consists of your current
 goal together with a heuristic selection of hundreds of facts (theorems) from the
@@ -859,11 +859,6 @@
 \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
-developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports the TPTP typed first-order format (TFF0). The
-remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
-
 \item[\labelitemi] \textbf{\textit{remote\_iprover}:} The
 remote version of iProver runs on Geoff Sutcliffe's Miami servers
 \cite{sutcliffe-2000}.
diff -r 25c1ff13dbdb -r 535ff1eac86c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 25 14:55:14 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 25 14:59:56 2019 +0200
@@ -52,7 +52,6 @@
   val eN : string
   val e_malesN : string
   val e_parN : string
-  val e_tofofN : string
   val ehohN : string
   val iproverN : string
   val leo2N : string
@@ -120,7 +119,6 @@
 val eN = "e"
 val e_malesN = "e_males"
 val e_parN = "e_par"
-val e_tofofN = "e_tofof"
 val ehohN = "ehoh"
 val iproverN = "iprover"
 val leo2N = "leo2"
@@ -422,8 +420,6 @@
 
 val waldmeister_conjecture_name = "conjecture_1"
 
-val tofof_fact_prefix = "fof_"
-
 fun is_same_term subst tm1 tm2 =
   let
     fun do_term_pair (AAbs (((var1, typ1), body1), args1)) (AAbs (((var2, typ2), body2), args2))
@@ -573,7 +569,7 @@
             if role' = Definition then
               (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
             else
-              (((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]), phi), "", [])
+              (((num, [s]), phi), "", [])
           | Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
       in
         [(name, role', phi, rule, map (rpair []) deps)]
@@ -603,8 +599,7 @@
                       phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq)
                    | _ => ((num, []), phi))
                  else
-                   ((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]),
-                    phi),
+                   ((num, [s]), phi),
                  role, "", [])
               | File_Source _ =>
                 (((num, map fst (find_formula_in_problem phi problem)), phi), role, "", [])
diff -r 25c1ff13dbdb -r 535ff1eac86c src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 14:55:14 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 14:59:56 2019 +0200
@@ -731,9 +731,6 @@
   remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
     [("refutation.", "end_refutation.")] [] Hypothesis
     (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *))
-val remote_e_tofof =
-  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
-    (K (((150, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *))
 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
 
 
@@ -771,8 +768,8 @@
 
 val atps =
   [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire,
-   z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_e_tofof, remote_iprover, remote_leo2,
-   remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
+   z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_iprover, remote_leo2, remote_leo3,
+   remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
 
 val _ = Theory.setup (fold add_atp atps)