removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)

--- a/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 14:51:16 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 14:55:14 2019 +0200
@@ -102,10 +102,10 @@
 historical.}
 %
 The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
-\cite{schulz-2002}, E-SInE \cite{sine}, 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
+\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
@@ -147,10 +147,10 @@
 relies on third-party automatic provers (ATPs and SMT solvers).
 
 Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and
-Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF,
-iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are
-available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers
-CVC3, CVC4, veriT, and Z3 can be run locally.
+Zipperposition can be run locally; in addition, AgsyHOL, E, E-ToFoF, iProver,
+LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are available
+remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC3,
+CVC4, veriT, and Z3 can be run locally.
 
 There are three main ways to install automatic provers on your machine:
 
@@ -859,10 +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\_sine}:} E-SInE is a metaprover
-developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff
-Sutcliffe's Miami servers.
-
 \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
@@ -897,9 +893,9 @@
 runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
-By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire,
-veriT, and Z3 in parallel, either locally or remotely---depending on the number
-of processor cores available and on which provers are actually installed. It is
+By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and
+Z3 in parallel, either locally or remotely---depending on the number of
+processor cores available and on which provers are actually installed. It is
 generally a good idea to run several provers in parallel.
 
 \opnodefault{prover}{string}

--- a/src/HOL/ATP.thy	Fri Oct 25 14:51:16 2019 +0200
+++ b/src/HOL/ATP.thy	Fri Oct 25 14:55:14 2019 +0200
@@ -137,6 +137,5 @@
 ML_file \<open>Tools/monomorph.ML\<close>
 ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
 ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
-ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 
 end

--- a/src/HOL/Sledgehammer.thy	Fri Oct 25 14:51:16 2019 +0200
+++ b/src/HOL/Sledgehammer.thy	Fri Oct 25 14:55:14 2019 +0200
@@ -16,6 +16,8 @@
 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
   by (erule contrapos_nn) (rule arg_cong)
 
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
+
 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
@@ -35,4 +37,7 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 
+lemma "1 + 1 = 2"
+  sledgehammer [iprover, overlord, dont_minimize, dont_preplay]
+
 end

--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 25 14:51:16 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 25 14:55:14 2019 +0200
@@ -52,7 +52,6 @@
   val eN : string
   val e_malesN : string
   val e_parN : string
-  val e_sineN : string
   val e_tofofN : string
   val ehohN : string
   val iproverN : string
@@ -121,7 +120,6 @@
 val eN = "e"
 val e_malesN = "e_males"
 val e_parN = "e_par"
-val e_sineN = "e_sine"
 val e_tofofN = "e_tofof"
 val ehohN = "ehoh"
 val iproverN = "iprover"

--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 14:51:16 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 14:55:14 2019 +0200
@@ -727,9 +727,6 @@
 val remote_vampire =
   remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
     (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
-val remote_e_sine =
-  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
-    (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
     [("refutation.", "end_refutation.")] [] Hypothesis
@@ -774,8 +771,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_sine, 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_e_tofof, remote_iprover, remote_leo2,
+   remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
 
 val _ = Theory.setup (fold add_atp atps)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Oct 25 14:51:16 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Oct 25 14:55:14 2019 +0200
@@ -177,7 +177,7 @@
 fun default_provers_param_value mode ctxt =
   [cvc4N] @
   (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @
-  [z3N, eN, spassN, veritN, e_sineN]
+  [z3N, eN, spassN, veritN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))