merged

--- a/src/HOL/Finite_Set.thy	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Mar 06 14:11:58 2024 +0100
@@ -1032,6 +1032,22 @@
 
 text \<open>Other properties of \<^const>\<open>fold\<close>:\<close>
 
+lemma finite_set_fold_single [simp]: "Finite_Set.fold f z {x} = f x z"
+proof -
+  have "fold_graph f z {x} (f x z)"
+    by (auto intro: fold_graph.intros)
+  moreover
+  {
+    fix X y
+    have "fold_graph f z X y \<Longrightarrow> (X = {} \<longrightarrow> y = z) \<and> (X = {x} \<longrightarrow> y = f x z)"
+      by (induct rule: fold_graph.induct) auto
+  }
+  ultimately have "(THE y. fold_graph f z {x} y) = f x z"
+    by blast
+  thus ?thesis
+    by (simp add: Finite_Set.fold_def)
+qed
+
 lemma fold_graph_image:
   assumes "inj_on g A"
   shows "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"

--- a/src/HOL/Library/Multiset.thy	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 06 14:11:58 2024 +0100
@@ -243,6 +243,9 @@
   with that show ?thesis by blast
 qed
 
+lemma count_gt_imp_in_mset: "count M x > n \<Longrightarrow> x \<in># M"
+  using count_greater_zero_iff by fastforce
+
 
 subsubsection \<open>Union\<close>
 
@@ -393,6 +396,11 @@
 abbreviation Max_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
 "Max_mset m \<equiv> Max (set_mset m)"
 
+lemma
+  Min_in_mset: "M \<noteq> {#} \<Longrightarrow> Min_mset M \<in># M" and
+  Max_in_mset: "M \<noteq> {#} \<Longrightarrow> Max_mset M \<in># M"
+  by simp+
+
 
 subsubsection \<open>Equality of multisets\<close>
 
@@ -684,6 +692,12 @@
     using A by (simp add: mset_subset_eq_add_mset_cancel)
 qed simp
 
+lemma nonempty_subseteq_mset_eq_single: "M \<noteq> {#} \<Longrightarrow> M \<subseteq># {#x#} \<Longrightarrow> M = {#x#}"
+  by (cases M) (metis single_is_union subset_mset.less_eqE)
+
+lemma nonempty_subseteq_mset_iff_single: "(M \<noteq> {#} \<and> M \<subseteq># {#x#} \<and> P) \<longleftrightarrow> M = {#x#} \<and> P"
+  by (cases M) (metis empty_not_add_mset nonempty_subseteq_mset_eq_single subset_mset.order_refl)
+
 
 subsubsection \<open>Intersection and bounded union\<close>
 
@@ -1374,6 +1388,9 @@
   unfolding \<open>M = M'\<close>
   using assms by (auto intro: filter_mset_cong0)
 
+lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
+  by (induct D) (simp add: multiset_eqI)
+
 
 subsubsection \<open>Size\<close>
 
@@ -1480,6 +1497,9 @@
   "M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
 by (metis add_diff_cancel_left' size_union mset_subset_eq_exists_conv)
 
+lemma size_lt_imp_ex_count_lt: "size M < size N \<Longrightarrow> \<exists>x \<in># N. count M x < count N x"
+  by (metis count_eq_zero_iff leD not_le_imp_less not_less_zero size_mset_mono subseteq_mset_def)
+
 
 subsection \<open>Induction and case splits\<close>
 
@@ -1644,6 +1664,9 @@
 lemma fold_mset_empty [simp]: "fold_mset f s {#} = s"
   by (simp add: fold_mset_def)
 
+lemma fold_mset_single [simp]: "fold_mset f s {#x#} = f x s"
+  by (simp add: fold_mset_def)
+
 context comp_fun_commute
 begin
 
@@ -1674,9 +1697,6 @@
   qed
 qed
 
-corollary fold_mset_single: "fold_mset f s {#x#} = f x s"
-  by simp
-
 lemma fold_mset_fun_left_comm: "f x (fold_mset f s M) = fold_mset f (f x s) M"
   by (induct M) (simp_all add: fun_left_comm)
 
@@ -1849,7 +1869,6 @@
   "image_mset f (filter_mset (\<lambda>x. P (f x)) M) = filter_mset P (image_mset f M)"
   by (induction M rule: multiset_induct) simp_all
 
-
 lemma image_mset_eq_plusD:
   "image_mset f A = B + C \<Longrightarrow> \<exists>B' C'. A = B' + C' \<and> B = image_mset f B' \<and> C = image_mset f C'"
 proof (induction A arbitrary: B C)
@@ -2278,7 +2297,7 @@
 qed
 
 
-subsection \<open>More properties of the replicate and repeat operations\<close>
+subsection \<open>More properties of the replicate, repeat, and image operations\<close>
 
 lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
   unfolding replicate_mset_def by (induct n) auto
@@ -2292,9 +2311,6 @@
 lemma count_le_replicate_mset_subset_eq: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
   by (auto simp add: mset_subset_eqI) (metis count_replicate_mset subseteq_mset_def)
 
-lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
-  by (induct D) simp_all
-
 lemma replicate_count_mset_eq_filter_eq: "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
   by (induct xs) auto
 
@@ -2354,6 +2370,195 @@
   then show thesis using A ..
 qed
 
+lemma count_image_mset_lt_imp_lt_raw:
+  assumes
+    "finite A" and
+    "A = set_mset M \<union> set_mset N" and
+    "count (image_mset f M) b < count (image_mset f N) b"
+  shows "\<exists>x. f x = b \<and> count M x < count N x"
+  using assms
+proof (induct A arbitrary: M N b rule: finite_induct)
+  case (insert x F)
+  note fin = this(1) and x_ni_f = this(2) and ih = this(3) and x_f_eq_m_n = this(4) and
+    cnt_b = this(5)
+
+  let ?Ma = "{#y \<in># M. y \<noteq> x#}"
+  let ?Mb = "{#y \<in># M. y = x#}"
+  let ?Na = "{#y \<in># N. y \<noteq> x#}"
+  let ?Nb = "{#y \<in># N. y = x#}"
+
+  have m_part: "M = ?Mb + ?Ma" and n_part: "N = ?Nb + ?Na"
+    using multiset_partition by blast+
+
+  have f_eq_ma_na: "F = set_mset ?Ma \<union> set_mset ?Na"
+    using x_f_eq_m_n x_ni_f by auto
+
+  show ?case
+  proof (cases "count (image_mset f ?Ma) b < count (image_mset f ?Na) b")
+    case cnt_ba: True
+    obtain xa where "f xa = b" and "count ?Ma xa < count ?Na xa"
+      using ih[OF f_eq_ma_na cnt_ba] by blast
+    thus ?thesis
+      by (metis count_filter_mset not_less0)
+  next
+    case cnt_ba: False
+    have fx_eq_b: "f x = b"
+      using cnt_b cnt_ba
+      by (subst (asm) m_part, subst (asm) n_part,
+          auto simp: filter_eq_replicate_mset split: if_splits)
+    moreover have "count M x < count N x"
+      using cnt_b cnt_ba
+      by (subst (asm) m_part, subst (asm) n_part,
+          auto simp: filter_eq_replicate_mset split: if_splits)
+    ultimately show ?thesis
+      by blast
+  qed
+qed auto
+
+lemma count_image_mset_lt_imp_lt:
+  assumes cnt_b: "count (image_mset f M) b < count (image_mset f N) b"
+  shows "\<exists>x. f x = b \<and> count M x < count N x"
+  by (rule count_image_mset_lt_imp_lt_raw[of "set_mset M \<union> set_mset N", OF _ refl cnt_b]) auto
+
+lemma count_image_mset_le_imp_lt_raw:
+  assumes
+    "finite A" and
+    "A = set_mset M \<union> set_mset N" and
+    "count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a"
+  shows "\<exists>b. f b = f a \<and> count M b < count N b"
+  using assms
+proof (induct A arbitrary: M N rule: finite_induct)
+  case (insert x F)
+  note fin = this(1) and x_ni_f = this(2) and ih = this(3) and x_f_eq_m_n = this(4) and
+    cnt_lt = this(5)
+
+  let ?Ma = "{#y \<in># M. y \<noteq> x#}"
+  let ?Mb = "{#y \<in># M. y = x#}"
+  let ?Na = "{#y \<in># N. y \<noteq> x#}"
+  let ?Nb = "{#y \<in># N. y = x#}"
+
+  have m_part: "M = ?Mb + ?Ma" and n_part: "N = ?Nb + ?Na"
+    using multiset_partition by blast+
+
+  have f_eq_ma_na: "F = set_mset ?Ma \<union> set_mset ?Na"
+    using x_f_eq_m_n x_ni_f by auto
+
+  show ?case
+  proof (cases "f x = f a")
+    case fx_ne_fa: False
+
+    have cnt_fma_fa: "count (image_mset f ?Ma) (f a) = count (image_mset f M) (f a)"
+      using fx_ne_fa by (subst (2) m_part) (auto simp: filter_eq_replicate_mset)
+    have cnt_fna_fa: "count (image_mset f ?Na) (f a) = count (image_mset f N) (f a)"
+      using fx_ne_fa by (subst (2) n_part) (auto simp: filter_eq_replicate_mset)
+    have cnt_ma_a: "count ?Ma a = count M a"
+      using fx_ne_fa by (subst (2) m_part) (auto simp: filter_eq_replicate_mset)
+    have cnt_na_a: "count ?Na a = count N a"
+      using fx_ne_fa by (subst (2) n_part) (auto simp: filter_eq_replicate_mset)
+
+    obtain b where fb_eq_fa: "f b = f a" and cnt_b: "count ?Ma b < count ?Na b"
+      using ih[OF f_eq_ma_na] cnt_lt unfolding cnt_fma_fa cnt_fna_fa cnt_ma_a cnt_na_a by blast
+    have fx_ne_fb: "f x \<noteq> f b"
+      using fb_eq_fa fx_ne_fa by simp
+
+    have cnt_ma_b: "count ?Ma b = count M b"
+      using fx_ne_fb by (subst (2) m_part) auto
+    have cnt_na_b: "count ?Na b = count N b"
+      using fx_ne_fb by (subst (2) n_part) auto
+
+    show ?thesis
+      using fb_eq_fa cnt_b unfolding cnt_ma_b cnt_na_b by blast
+  next
+    case fx_eq_fa: True
+    show ?thesis
+    proof (cases "x = a")
+      case x_eq_a: True
+      have "count (image_mset f ?Ma) (f a) + count ?Na a
+        < count (image_mset f ?Na) (f a) + count ?Ma a"
+        using cnt_lt x_eq_a by (subst (asm) (1 2) m_part, subst (asm) (1 2) n_part,
+            auto simp: filter_eq_replicate_mset)
+      thus ?thesis
+        using ih[OF f_eq_ma_na] by (metis count_filter_mset nat_neq_iff)
+    next
+      case x_ne_a: False
+      show ?thesis
+      proof (cases "count M x < count N x")
+        case True
+        thus ?thesis
+          using fx_eq_fa by blast
+     next
+        case False
+        hence cnt_x: "count M x \<ge> count N x"
+          by fastforce
+        have "count M x + count (image_mset f ?Ma) (f a) + count ?Na a
+          < count N x + count (image_mset f ?Na) (f a) + count ?Ma a"
+          using cnt_lt x_ne_a fx_eq_fa by (subst (asm) (1 2) m_part, subst (asm) (1 2) n_part,
+            auto simp: filter_eq_replicate_mset)
+        hence "count (image_mset f ?Ma) (f a) + count ?Na a
+          < count (image_mset f ?Na) (f a) + count ?Ma a"
+          using cnt_x by linarith
+        thus ?thesis
+          using ih[OF f_eq_ma_na] by (metis count_filter_mset nat_neq_iff)
+      qed
+    qed
+  qed
+qed auto
+
+lemma count_image_mset_le_imp_lt:
+  assumes
+    "count (image_mset f M) (f a) \<le> count (image_mset f N) (f a)" and
+    "count M a > count N a"
+  shows "\<exists>b. f b = f a \<and> count M b < count N b"
+  using assms by (auto intro: count_image_mset_le_imp_lt_raw[of "set_mset M \<union> set_mset N"])
+
+lemma size_filter_unsat_elem:
+  assumes "x \<in># M" and "\<not> P x"
+  shows "size {#x \<in># M. P x#} < size M"
+proof -
+  have "size (filter_mset P M) \<noteq> size M"
+    using assms by (metis add.right_neutral add_diff_cancel_left' count_filter_mset mem_Collect_eq
+      multiset_partition nonempty_has_size set_mset_def size_union)
+  then show ?thesis
+    by (meson leD nat_neq_iff size_filter_mset_lesseq)
+qed
+
+lemma size_filter_ne_elem: "x \<in># M \<Longrightarrow> size {#y \<in># M. y \<noteq> x#} < size M"
+  by (simp add: size_filter_unsat_elem[of x M "\<lambda>y. y \<noteq> x"])
+
+lemma size_eq_ex_count_lt:
+  assumes
+    sz_m_eq_n: "size M = size N" and
+    m_eq_n: "M \<noteq> N"
+  shows "\<exists>x. count M x < count N x"
+proof -
+  obtain x where "count M x \<noteq> count N x"
+    using m_eq_n by (meson multiset_eqI)
+  moreover
+  {
+    assume "count M x < count N x"
+    hence ?thesis
+      by blast
+  }
+  moreover
+  {
+    assume cnt_x: "count M x > count N x"
+
+    have "size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} =
+      size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}"
+      using sz_m_eq_n multiset_partition by (metis size_union)
+    hence sz_m_minus_x: "size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}"
+      using cnt_x by (simp add: filter_eq_replicate_mset)
+    then obtain y where "count {#y \<in># M. y \<noteq> x#} y < count {#y \<in># N. y \<noteq> x#} y"
+      using size_lt_imp_ex_count_lt[OF sz_m_minus_x] by blast
+    hence "count M y < count N y"
+      by (metis count_filter_mset less_asym)
+    hence ?thesis
+      by blast
+  }
+  ultimately show ?thesis
+    by fastforce
+qed
+
 
 subsection \<open>Big operators\<close>
 
@@ -2571,7 +2776,6 @@
 lemma Union_image_single_mset[simp]: "\<Sum>\<^sub># (image_mset (\<lambda>x. {#x#}) m) = m"
 by(induction m) auto
 
-
 context comm_monoid_mult
 begin
 

--- a/src/HOL/Library/Multiset_Order.thy	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Wed Mar 06 14:11:58 2024 +0100
@@ -853,4 +853,63 @@
 
 end
 
+lemma add_mset_lt_left_lt: "a < b \<Longrightarrow> add_mset a A < add_mset b A"
+  by fastforce
+
+lemma add_mset_le_left_le: "a \<le> b \<Longrightarrow> add_mset a A \<le> add_mset b A" for a :: "'a :: linorder"
+  by fastforce
+
+lemma add_mset_lt_right_lt: "A < B \<Longrightarrow> add_mset a A < add_mset a B"
+  by fastforce
+
+lemma add_mset_le_right_le: "A \<le> B \<Longrightarrow> add_mset a A \<le> add_mset a B"
+  by fastforce
+
+lemma add_mset_lt_lt_lt:
+  assumes a_lt_b: "a < b" and A_le_B: "A < B"
+  shows "add_mset a A < add_mset b B"
+  by (rule less_trans[OF add_mset_lt_left_lt[OF a_lt_b] add_mset_lt_right_lt[OF A_le_B]])
+
+lemma add_mset_lt_lt_le: "a < b \<Longrightarrow> A \<le> B \<Longrightarrow> add_mset a A < add_mset b B"
+  using add_mset_lt_lt_lt le_neq_trans by fastforce
+
+lemma add_mset_lt_le_lt: "a \<le> b \<Longrightarrow> A < B \<Longrightarrow> add_mset a A < add_mset b B" for a :: "'a :: linorder"
+  using add_mset_lt_lt_lt by (metis add_mset_lt_right_lt le_less)
+
+lemma add_mset_le_le_le:
+  fixes a :: "'a :: linorder"
+  assumes a_le_b: "a \<le> b" and A_le_B: "A \<le> B"
+  shows "add_mset a A \<le> add_mset b B"
+  by (rule order.trans[OF add_mset_le_left_le[OF a_le_b] add_mset_le_right_le[OF A_le_B]])
+
+lemma Max_lt_imp_lt_mset:
+  assumes n_nemp: "N \<noteq> {#}" and max: "Max_mset M < Max_mset N" (is "?max_M < ?max_N")
+  shows "M < N"
+proof (cases "M = {#}")
+  case m_nemp: False
+
+  have max_n_in_n: "?max_N \<in># N"
+    using n_nemp by simp
+  have max_n_nin_m: "?max_N \<notin># M"
+    using max Max_ge leD by auto
+
+  have "M \<noteq> N"
+    using max by auto
+  moreover
+  {
+    fix y
+    assume "count N y < count M y"
+    hence "y \<in># M"
+      by (simp add: count_inI)
+    hence "?max_M \<ge> y"
+      by simp
+    hence "?max_N > y"
+      using max by auto
+    hence "\<exists>x > y. count M x < count N x"
+      using max_n_nin_m max_n_in_n count_inI by force
+  }
+  ultimately show ?thesis
+    unfolding less_multiset\<^sub>H\<^sub>O by blast
+qed (auto simp: n_nemp)
+
 end

--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Mar 06 14:11:58 2024 +0100
@@ -6,6 +6,7 @@
 
 signature ATP_UTIL =
 sig
+  val proof_cartouches: bool Config.T
   val timestamp : unit -> string
   val hashw : word * word -> word
   val hashw_string : string * word -> word
@@ -18,7 +19,7 @@
   val find_enclosed : string -> string -> string -> string list
   val nat_subscript : int -> string
   val unquote_tvar : string -> string
-  val maybe_quote : Keyword.keywords -> string -> string
+  val maybe_quote : Proof.context -> string -> string
   val string_of_ext_time : bool * Time.time -> string
   val string_of_time : Time.time -> string
   val type_instance : theory -> typ -> typ -> bool
@@ -56,6 +57,8 @@
 structure ATP_Util : ATP_UTIL =
 struct
 
+val proof_cartouches = Attrib.setup_config_bool \<^binding>\<open>atp_proof_cartouches\<close> (K false)
+
 fun forall2 _ [] [] = true
   | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
   | forall2 _ _ _ = false
@@ -138,11 +141,15 @@
 val unquery_var = perhaps (try (unprefix "?"))
 
 val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
-fun maybe_quote keywords y =
-  let val s = YXML.content_of y in
+fun maybe_quote ctxt y =
+  let
+    val s = YXML.content_of y
+    val is_literal = (Keyword.is_literal o Thy_Header.get_keywords') ctxt
+    val gen_quote = if Config.get ctxt proof_cartouches then cartouche else quote
+  in
     y |> ((not (is_long_identifier (unquote_tvar s)) andalso
            not (is_long_identifier (unquery_var s))) orelse
-           Keyword.is_literal keywords s) ? quote
+           is_literal s) ? gen_quote
   end
 
 fun string_of_ext_time (plus, time) =

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 06 14:11:58 2024 +0100
@@ -202,7 +202,6 @@
     val time_start = Time.now ()
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
-    val keywords = Thy_Header.get_keywords thy
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
          boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
          overlord, spy, user_axioms, assms, whacks, merge_type_vars,
@@ -342,7 +341,7 @@
 
     val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
     fun monotonicity_message Ts extra =
-      let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in
+      let val pretties = map (pretty_maybe_quote ctxt o pretty_for_type ctxt) Ts in
         Pretty.blk (0,
           Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @
           pretty_serial_commas "and" pretties @ [Pretty.brk 1] @

--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Mar 06 14:11:58 2024 +0100
@@ -181,8 +181,8 @@
     fun standard_blocks s = map (Pretty.block o cons (Pretty.str (s ^ " ")))
     val (primary_cards, secondary_cards, maxes, iters, miscs) =
       quintuple_for_scope
-        (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o pretty_for_type ctxt)
-        (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o Syntax.pretty_term ctxt)
+        (fn ctxt => pretty_maybe_quote ctxt o pretty_for_type ctxt)
+        (fn ctxt => pretty_maybe_quote ctxt o Syntax.pretty_term ctxt)
         Pretty.str scope
   in
     standard_blocks "card" primary_cards @

--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Mar 06 14:11:58 2024 +0100
@@ -69,7 +69,7 @@
   val eta_expand : typ list -> term -> int -> term
   val DETERM_TIMEOUT : Time.time -> tactic -> tactic
   val indent_size : int
-  val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T
+  val pretty_maybe_quote : Proof.context -> Pretty.T -> Pretty.T
   val hash_term : term -> int
   val spying : bool -> (unit -> Proof.state * int * string) -> unit
 end;
@@ -279,9 +279,9 @@
 
 val maybe_quote = ATP_Util.maybe_quote
 
-fun pretty_maybe_quote keywords pretty =
+fun pretty_maybe_quote ctxt pretty =
   let val s = Pretty.unformatted_string_of pretty
-  in if maybe_quote keywords s = s then pretty else Pretty.quote pretty end
+  in if maybe_quote ctxt s = s then pretty else Pretty.quote pretty end
 
 val hashw = ATP_Util.hashw
 val hashw_string = ATP_Util.hashw_string

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Mar 06 14:11:58 2024 +0100
@@ -61,6 +61,7 @@
 val TF0 = TFF (Monomorphic, Without_FOOL)
 val TF1 = TFF (Polymorphic, Without_FOOL)
 val TX0 = TFF (Monomorphic, With_FOOL {with_ite = true, with_let = true})
+val TX0_MINUS = TFF (Monomorphic, With_FOOL {with_ite = false, with_let = false})
 val TX1 = TFF (Polymorphic, With_FOOL {with_ite = true, with_let = true})
 val TH0 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice)
 val TH0_MINUS = THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice)
@@ -177,7 +178,9 @@
 
 (* E *)
 
-val e_config : atp_config =
+local
+
+fun make_e_config max_new_mono_insts good_slices : atp_config =
   {exec = (["E_HOME"], ["eprover-ho", "eprover"]),
    arguments = fn abduce => fn _ => fn extra_options => fn timeout => fn problem =>
      ["--tstp-in --tstp-out --silent " ^
@@ -195,8 +198,11 @@
      known_szs_status_failures,
    prem_role = Conjecture,
    generate_isabelle_info = false,
-   good_slices =
-     let
+   good_slices = K good_slices,
+   good_max_mono_iters = default_max_mono_iters,
+   good_max_new_mono_instances = max_new_mono_insts}
+
+val old_e_config : atp_config = make_e_config default_max_new_mono_instances (let
        val (format, type_enc, lam_trans, extra_options) =
          if string_ord (getenv "E_VERSION", "3.0") <> LESS then
            (* '$ite' support appears to be unsound. *)
@@ -207,17 +213,47 @@
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule")
      in
        (* FUDGE *)
-       K [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
-         ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)),
-         ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
-         ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)),
-         ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
-         ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))]
-     end,
-   good_max_mono_iters = default_max_mono_iters,
-   good_max_new_mono_instances = default_max_new_mono_instances}
+       [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
+        ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)),
+        ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
+        ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)),
+        ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
+        ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))]
+     end)
 
-val e = (eN, fn () => e_config)
+val new_e_config : atp_config =
+  (* FUDGE: this solved 950/1500 (63.33 %) using MePo when testing *)
+  make_e_config 128
+    [(((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
+     (((2, false, false, 1024, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
+     (((2, false, false,  128, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
+     (((2, false, false, 2048, meshN), (TF0, "mono_native", combsN, false, ""))),
+     (((2, false, false,  512, meshN), (TF0, "mono_native", liftingN, false, ""))),
+     (((2, false, false, 1024, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
+     (((2, false, false,   64, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
+     (((2, false, false,  512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
+     (((2, false, false,   32, meshN), (TF0, "mono_native", liftingN, false, ""))),
+     (((2, false, false, 2048, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
+     (((2, false, false,  256, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
+     (((2, false, false,  512, meshN), (TF0, "mono_native", combsN, false, ""))),
+     (((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, ""))),
+     (((2, false, false,   16, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
+     (((2, false, false,  512, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
+     (((2, false, false,   64, meshN), (TF0, "mono_native", liftingN, false, ""))),
+     (((2, false, false,  128, meshN), (TF0, "mono_native", combsN, false, ""))),
+     (((2, false, false, 2048, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
+     (((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", combsN, false, ""))),
+     (((2, false, false, 2048, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, "")))]
+
+in
+
+val e = (eN, fn () =>
+  if string_ord (getenv "E_VERSION", "3.0") <> LESS then
+    new_e_config
+  else
+    old_e_config)
+
+end
 
 
 (* iProver *)
@@ -423,9 +459,8 @@
    ((2, false, false, 128, meshN), (TX1, "mono_native", liftingN, false, no_sosN))]
 
 val new_vampire_config : atp_config =
-  let val infinity = 1000 in
-    (* FUDGE: this solved 998/1500 (66.53 %) using MePo when testing *)
-    make_vampire_config new_vampire_basic_options 256
+  (* FUDGE: this solved 998/1500 (66.53 %) using MePo when testing *)
+  make_vampire_config new_vampire_basic_options 256
     [(((2, false, false,  512, meshN), (TX0, "mono_native_fool", liftingN, false, ""))),
      (((2, false, false, 2048, meshN), (TX0, "mono_native_fool", combsN, false, ""))),
      (((2, false, false,  128, meshN), (TX0, "mono_native_fool", liftingN, false, ""))),
@@ -445,7 +480,6 @@
      (((2, false, false,  512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
      (((2, false, false,  512, meshN), (TX0, "mono_native_fool", combsN, false, ""))),
      (((2, false, false, 1024, meshN), (TX1, "poly_native_fool", combsN, false, "")))]
-  end
 
 in
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Wed Mar 06 14:11:58 2024 +0100
@@ -373,7 +373,6 @@
 
 fun string_of_isar_proof ctxt0 i n proof =
   let
-    val keywords = Thy_Header.get_keywords' ctxt0
 
     (* Make sure only type constraints inserted by the type annotation code are printed. *)
     val ctxt = ctxt0
@@ -408,7 +407,7 @@
             |> annotate_types_in_term ctxt
             |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
             |> simplify_spaces
-            |> maybe_quote keywords),
+            |> maybe_quote ctxt),
        ctxt |> perhaps (try (Proof_Context.augment term)))
 
     fun using_facts [] [] = ""
@@ -425,8 +424,8 @@
       end
 
     fun of_free (s, T) =
-      maybe_quote keywords s ^ " :: " ^
-      maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
+      Proof_Context.print_name ctxt s ^ " :: " ^
+      maybe_quote ctxt (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
 
     fun add_frees xs (s, ctxt) =
       (s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs))

--- a/src/HOL/ex/Sketch_and_Explore.thy	Tue Mar 05 23:06:18 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Wed Mar 06 14:11:58 2024 +0100
@@ -18,7 +18,7 @@
   in (fixes, assms, concl) end;
 
 fun maybe_quote ctxt =
-  ATP_Util.maybe_quote (Thy_Header.get_keywords' ctxt);
+  ATP_Util.maybe_quote ctxt;
 
 fun print_typ ctxt T =
   T