merged;

--- a/Admin/components/components.sha1	Mon Aug 07 20:05:23 2017 +0200
+++ b/Admin/components/components.sha1	Mon Aug 07 21:43:33 2017 +0200
@@ -34,6 +34,7 @@
 e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
 b98a98025d1f7e560ca6864a53296137dae736b4  e-1.6.tar.gz
 c11b25c919e2ec44fe2b6ac2086337b456344e97  e-1.8.tar.gz
+6b962a6b4539b7ca4199977973c61a8c98a492e8  e-2.0.tar.gz
 6d34b18ca0aa1e10bab6413045d079188c0e2dfb  exec_process-1.0.1.tar.gz
 8b9bffd10e396d965e815418295f2ee2849bea75  exec_process-1.0.2.tar.gz
 e6aada354da11e533af2dee3dcdd96c06479b053  exec_process-1.0.3.tar.gz

--- a/Admin/components/main	Mon Aug 07 20:05:23 2017 +0200
+++ b/Admin/components/main	Mon Aug 07 21:43:33 2017 +0200
@@ -2,7 +2,7 @@
 bash_process-1.2.1
 csdp-6.x
 cvc4-1.5
-e-1.8
+e-2.0
 isabelle_fonts-20160830
 jdk-8u131
 jedit_build-20170319

--- a/src/Doc/Sledgehammer/document/root.tex	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Aug 07 21:43:33 2017 +0200
@@ -197,8 +197,8 @@
 for Alt-Ergo, set the
 environment variable \texttt{WHY3\_HOME} to the directory that contains the
 \texttt{why3} executable.
-Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 1.8,
-LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.%
+Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0,
+LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 4.0.%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
 reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
 recent than 9.0 or 11.5.}%
@@ -206,7 +206,7 @@
 versions might not work well with Sledgehammer. Ideally,
 you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
+\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0'').
 
 Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
 variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},

--- a/src/HOL/ATP.thy	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/ATP.thy	Mon Aug 07 21:43:33 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Automatic Theorem Provers (ATPs)\<close>
 
 theory ATP
-imports Meson
+  imports Meson
 begin
 
 subsection \<open>ATP problems and proofs\<close>

--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 07 21:43:33 2017 +0200
@@ -2470,53 +2470,39 @@
 proof safe
   fix a b :: 'b
   show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-    if "box a b = {}"
+    if "box a b = {}" for a b
     apply (rule_tac x=f in exI)
-    using assms that
-    apply (auto simp: content_eq_0_interior)
-    done
+    using assms that by (auto simp: content_eq_0_interior)
   {
-    fix c g
-    fix k :: 'b
-    assume as: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
+    fix c g and k :: 'b
+    assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
     assume k: "k \<in> Basis"
     show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-      "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
-      apply (rule_tac[!] x=g in exI)
-      using as(1) integrable_split[OF as(2) k]
-      apply auto
-      done
+         "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
+       apply (rule_tac[!] x=g in exI)
+      using fg integrable_split[OF g k] by auto
   }
-  fix c k g1 g2
-  assume as: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-    "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
-  assume k: "k \<in> Basis"
-  let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
   show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-    apply (rule_tac x="?g" in exI)
-    apply safe
-  proof goal_cases
-    case (1 x)
-    then show ?case
-      apply -
-      apply (cases "x\<bullet>k=c")
-      apply (case_tac "x\<bullet>k < c")
-      using as assms
-      apply auto
-      done
-  next
-    case 2
-    presume "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-      and "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-    then guess h1 h2 unfolding integrable_on_def by auto
-    from has_integral_split[OF this k] show ?case
-      unfolding integrable_on_def by auto
-  next
-    show "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-      apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]])
-      using k as(2,4)
-      apply auto
-      done
+    if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" 
+      and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+      and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" 
+      and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" 
+      and k: "k \<in> Basis"
+    for c k g1 g2
+  proof -
+    let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+    show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+    proof (intro exI conjI ballI)
+      show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
+        by (auto simp: that assms fg1 fg2)
+      show "?g integrable_on cbox a b"
+      proof -
+        have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
+          by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
+        with has_integral_split[OF _ _ k] show ?thesis
+          unfolding integrable_on_def by blast
+      qed
+    qed
   qed
 qed
 
@@ -2531,18 +2517,16 @@
 lemma approximable_on_division:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
   assumes "0 \<le> e"
-    and "d division_of (cbox a b)"
-    and "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
+    and d: "d division_of (cbox a b)"
+    and f: "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
   obtains g where "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
 proof -
-  note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_approximable[OF assms(1)] assms(2)]
-  from assms(3) this[unfolded comm_monoid_set_F_and, of f] division_of_finite[OF assms(2)]
-  guess g by auto
-  then show thesis
-    apply -
-    apply (rule that[of g])
-    apply auto
-    done
+  note * = comm_monoid_set.operative_division
+             [OF comm_monoid_set_and operative_approximable[OF \<open>0 \<le> e\<close>] d]
+  have "finite d"
+    by (rule division_of_finite[OF d])
+  with f *[unfolded comm_monoid_set_F_and, of f] that show thesis
+    by auto
 qed
 
 lemma integrable_continuous:
@@ -3608,8 +3592,8 @@
 lemma fundamental_theorem_of_calculus_interior:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a \<le> b"
-    and "continuous_on {a .. b} f"
-    and "\<forall>x\<in>{a <..< b}. (f has_vector_derivative f'(x)) (at x)"
+    and contf: "continuous_on {a .. b} f"
+    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
   shows "(f' has_integral (f b - f a)) {a .. b}"
 proof -
   {
@@ -3637,22 +3621,22 @@
   { presume "\<And>e. e > 0 \<Longrightarrow> ?P e" then show ?thesis unfolding has_integral_factor_content_real by auto }
   fix e :: real
   assume e: "e > 0"
-  note assms(3)[unfolded has_vector_derivative_def has_derivative_at_alt ball_conj_distrib]
-  note conjunctD2[OF this]
-  note bounded=this(1) and this(2)
-  from this(2) have "\<forall>x\<in>box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
-    norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
-    apply -
-    apply safe
-    apply (erule_tac x=x in ballE)
-    apply (erule_tac x="e/2" in allE)
-    using e
-    apply auto
-    done
-  note this[unfolded bgauge_existence_lemma]
-  from choice[OF this] guess d ..
-  note conjunctD2[OF this[rule_format]]
-  note d = this[rule_format]
+  note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
+  have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
+    using derf_exp by simp
+  have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
+       (is "\<forall>x \<in> box a b. ?Q x")
+  proof
+    fix x assume x: "x \<in> box a b"
+    show "?Q x"
+      apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
+      using x e by auto
+  qed
+  from this [unfolded bgauge_existence_lemma]
+  obtain d where d: "\<And>x. 0 < d x"
+     "\<And>x y. \<lbrakk>x \<in> box a b; norm (y - x) < d x\<rbrakk>
+               \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e / 2 * norm (y - x)"
+    by metis
   have "bounded (f ` cbox a b)"
     apply (rule compact_imp_bounded compact_continuous_image)+
     using compact_cbox assms
@@ -3683,7 +3667,7 @@
         apply (auto simp add: field_simps)
         done
     qed
-    then guess l .. note l = conjunctD2[OF this]
+    then obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b - a) / 8" by metis
     show ?thesis
       apply (rule_tac x="min k l" in exI)
       apply safe
@@ -3698,24 +3682,28 @@
         by (rule norm_triangle_ineq4)
       also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
       proof (rule add_mono)
-        have "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
-          using as' by auto
-        then show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8"
-          apply -
-          apply (rule order_trans[OF _ l(2)])
+        have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
           unfolding norm_scaleR
           apply (rule mult_right_mono)
-          apply auto
-          done
+          using as' by auto
+        also have "... \<le> e * (b - a) / 8"
+          by (rule l)
+        finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8" .
       next
-        show "norm (f c - f a) \<le> e * (b - a) / 8"
-          apply (rule less_imp_le)
-          apply (cases "a = c")
-          defer
-          apply (rule k(2)[unfolded dist_norm])
-          using as' e ab
-          apply (auto simp add: field_simps)
-          done
+        have "norm (f c - f a) < e * (b - a) / 8"
+        proof (cases "a = c")
+          case True
+          then show ?thesis
+            using \<open>0 < e * (b - a) / 8\<close> by auto
+        next
+          case False
+          show ?thesis
+            apply (rule k(2)[unfolded dist_norm])
+            using as' False
+             apply (auto simp add: field_simps)
+            done
+        qed
+        then show "norm (f c - f a) \<le> e * (b - a) / 8" by simp
       qed
       finally show "norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
         unfolding content_real[OF as(1)] by auto
@@ -3804,7 +3792,7 @@
     note p = tagged_division_ofD[OF as(1)]
     have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
       using as by auto
-    note * = additive_tagged_division_1'[OF assms(1) as(1), symmetric]
+    note * = additive_tagged_division_1[OF assms(1) as(1), symmetric]
     have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
       by arith
     show ?case
@@ -3964,7 +3952,8 @@
             qed
             have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
             proof -
-              guess u v using p(4)[OF that] by (elim exE) note uv=this
+              obtain u v where uv: "k = cbox u v"
+                using \<open>(b, k) \<in> p\<close> p(4) by blast
               have *: "u \<le> v"
                 using p(2)[OF that] unfolding uv by auto
               have u: "v = b"

--- a/src/HOL/Analysis/Tagged_Division.thy	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Aug 07 21:43:33 2017 +0200
@@ -1836,15 +1836,6 @@
 lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
   by (meson zero_less_one)
 
-lemma additive_tagged_division_1':
-  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
-  assumes "a \<le> b"
-    and "p tagged_division_of {a..b}"
-  shows "sum (\<lambda>(x,k). f (Sup k) - f(Inf k)) p = f b - f a"
-  using additive_tagged_division_1[OF _ assms(2), of f]
-  using assms(1)
-  by auto
-
 subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
 
 definition fine  (infixr "fine" 46)

--- a/src/HOL/Equiv_Relations.thy	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/Equiv_Relations.thy	Mon Aug 07 21:43:33 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Equivalence Relations in Higher-Order Set Theory\<close>
 
 theory Equiv_Relations
-  imports Groups_Big Relation
+  imports Groups_Big
 begin
 
 subsection \<open>Equivalence relations -- set version\<close>

--- a/src/HOL/Groups_Big.thy	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Aug 07 21:43:33 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Big sum and product over finite (non-empty) sets\<close>
 
 theory Groups_Big
-  imports Finite_Set Power
+  imports Power
 begin
 
 subsection \<open>Generic monoid operation over a set\<close>

--- a/src/HOL/Lattices_Big.thy	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Mon Aug 07 21:43:33 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
 
 theory Lattices_Big
-imports Finite_Set Option
+  imports Option
 begin
 
 subsection \<open>Generic lattice operations over a set\<close>

--- a/src/HOL/Option.thy	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/Option.thy	Mon Aug 07 21:43:33 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Datatype option\<close>
 
 theory Option
-imports Lifting Finite_Set
+  imports Lifting
 begin
 
 datatype 'a option =

--- a/src/HOL/Partial_Function.thy	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/Partial_Function.thy	Mon Aug 07 21:43:33 2017 +0200
@@ -5,8 +5,8 @@
 section \<open>Partial Function Definitions\<close>
 
 theory Partial_Function
-imports Complete_Partial_Order Fun_Def_Base Option
-keywords "partial_function" :: thy_decl
+  imports Complete_Partial_Order Option
+  keywords "partial_function" :: thy_decl
 begin
 
 named_theorems partial_function_mono "monotonicity rules for partial function definitions"

--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 07 20:05:23 2017 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 07 21:43:33 2017 +0200
@@ -207,8 +207,6 @@
 
 (* E *)
 
-fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
-
 val e_smartN = "smart"
 val e_autoN = "auto"
 val e_fun_weightN = "fun_weight"
@@ -277,23 +275,19 @@
       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
     end
 
+val e_tff0 = TFF Monomorphic
+
 val e_config : atp_config =
-  {exec = fn full_proofs => (["E_HOME"],
-     if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"]
-     else ["eprover"]),
-   arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name =>
+  {exec = fn _ => (["E_HOME"], ["eprover"]),
+   arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
-       (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
-       "--tstp-in --tstp-out --silent " ^
+       "--auto-schedule --tstp-in --tstp-out --silent " ^
        e_selection_weight_arguments ctxt heuristic sel_weights ^
        e_term_order_info_arguments gen_weights gen_prec ord_info ^
        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
-       (if full_proofs orelse not (is_e_at_least_1_8 ()) then
-          " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2")
-        else
-          " --proof-object=1") ^
-       " " ^ file_name,
+       " --proof-object=1 " ^
+       file_name,
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
      tstp_proof_delims,
@@ -306,14 +300,14 @@
      let val heuristic = Config.get ctxt e_selection_heuristic in
        (* FUDGE *)
        if heuristic = e_smartN then
-         [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
-          (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
-          (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
-          (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
-          (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)),
-          (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))]
+         [(0.15, (((128, meshN), e_tff0, "mono_native", combsN, false), e_fun_weightN)),
+          (0.15, (((128, mashN), e_tff0, "mono_native", combsN, false), e_sym_offset_weightN)),
+          (0.15, (((91, mepoN), e_tff0, "mono_native", combsN, false), e_autoN)),
+          (0.15, (((1000, meshN), e_tff0, "poly_guards??", combsN, false), e_sym_offset_weightN)),
+          (0.15, (((256, mepoN), e_tff0, "mono_native", liftingN, false), e_fun_weightN)),
+          (0.25, (((64, mashN), e_tff0, "mono_native", combsN, false), e_fun_weightN))]
        else
-         [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
+         [(1.0, (((500, ""), e_tff0, "mono_native", combsN, false), heuristic))]
      end,
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
@@ -456,9 +450,8 @@
 val spass_extra_options =
   Attrib.setup_config_string @{binding atp_spass_extra_options} (K "")
 
-(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
 val spass_config : atp_config =
-  {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
+  {exec = K (["SPASS_HOME"], ["SPASS"]),
    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
        fn file_name => fn _ =>
        "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
@@ -710,7 +703,7 @@
     (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_e =
   remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
-    (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
+    (K (((750, ""), e_tff0, "mono_native", combsN, false), "") (* FUDGE *))
 val remote_iprover =
   remotify_atp iprover "iProver" ["0.99"]
     (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
@@ -724,7 +717,7 @@
   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
     (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["4.0", "3.0", "2.6"]
+  remotify_atp vampire "Vampire" ["4.2", "4.0"]
     (K (((400, ""), vampire_tff0, "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