# HG changeset patch
# User wenzelm
# Date 1638617931 -3600
# Node ID e8935405f08236a41e943fec320164c0896b7633
# Parent  98d2b3375258493c82f28d012a0d7b70b1022420# Parent  7b0a241732c1a12365962501d28fe403fa656c04
merged

diff -r 98d2b3375258 -r e8935405f082 CONTRIBUTORS
--- a/CONTRIBUTORS	Sat Dec 04 12:38:32 2021 +0100
+++ b/CONTRIBUTORS	Sat Dec 04 12:38:51 2021 +0100
@@ -3,6 +3,10 @@
 listed as an author in one of the source files of this Isabelle distribution.
 
 
+Contributions to this Isabelle version
+--------------------------------------
+
+
 Contributions to Isabelle2021-1
 -------------------------------
 
diff -r 98d2b3375258 -r e8935405f082 NEWS
--- a/NEWS	Sat Dec 04 12:38:32 2021 +0100
+++ b/NEWS	Sat Dec 04 12:38:51 2021 +0100
@@ -4,6 +4,31 @@
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
+New in this Isabelle version
+----------------------------
+
+*** HOL ***
+
+* Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
+  type class preorder.
+
+* Theory "HOL-Library.Multiset":
+  - Consolidated operation and fact names.
+        multp ~> multp_code
+        multeqp ~> multeqp_code
+        multp_cancel_add_mset ~> multp_cancel_add_mset0
+        multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
+        multp_code_iff ~> multp_code_iff_mult
+        multeqp_code_iff ~> multeqp_code_iff_reflcl_mult
+    Minor INCOMPATIBILITY.
+  - Moved mult1_lessE out of preorder type class and add explicit
+    assumption. Minor INCOMPATIBILITY.
+  - Added predicate multp equivalent to set mult. Reuse name previously
+    used for what is now called multp_code. Minor INCOMPATIBILITY.
+  - Lifted multiple lemmas from mult to multp.
+  - Redefined less_multiset to be based on multp. INCOMPATIBILITY.
+
+
 New in Isabelle2021-1 (December 2021)
 -------------------------------------
 
diff -r 98d2b3375258 -r e8935405f082 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Dec 04 12:38:51 2021 +0100
@@ -4,12 +4,13 @@
     Author:     Jasmin Blanchette, Inria, LORIA, MPII
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Mathias Fleury, MPII
+    Author:     Martin Desharnais, MPI-INF Saarbruecken
 *)
 
 section \<open>(Finite) Multisets\<close>
 
 theory Multiset
-imports Cancellation
+  imports Cancellation
 begin
 
 subsection \<open>The type of multisets\<close>
@@ -2788,8 +2789,6 @@
 
 subsection \<open>The multiset order\<close>
 
-subsubsection \<open>Well-foundedness\<close>
-
 definition mult1 :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
   "mult1 r = {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and>
       (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}"
@@ -2797,6 +2796,9 @@
 definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
   "mult r = (mult1 r)\<^sup>+"
 
+definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "multp r M N \<longleftrightarrow> (M, N) \<in> mult {(x, y). r x y}"
+
 lemma mult1I:
   assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
   shows "(N, M) \<in> mult1 r"
@@ -2809,14 +2811,29 @@
 
 lemma mono_mult1:
   assumes "r \<subseteq> r'" shows "mult1 r \<subseteq> mult1 r'"
-unfolding mult1_def using assms by blast
+  unfolding mult1_def using assms by blast
 
 lemma mono_mult:
   assumes "r \<subseteq> r'" shows "mult r \<subseteq> mult r'"
-unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+  unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+
+lemma mono_multp[mono]: "r \<le> r' \<Longrightarrow> multp r \<le> multp r'"
+  unfolding le_fun_def le_bool_def
+proof (intro allI impI)
+  fix M N :: "'a multiset"
+  assume "\<forall>x xa. r x xa \<longrightarrow> r' x xa"
+  hence "{(x, y). r x y} \<subseteq> {(x, y). r' x y}"
+    by blast
+  thus "multp r M N \<Longrightarrow> multp r' M N"
+    unfolding multp_def
+    by (fact mono_mult[THEN subsetD, rotated])
+qed
 
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
-by (simp add: mult1_def)
+  by (simp add: mult1_def)
+
+
+subsubsection \<open>Well-foundedness\<close>
 
 lemma less_add:
   assumes mult1: "(N, add_mset a M0) \<in> mult1 r"
@@ -2918,11 +2935,15 @@
   qed
 qed
 
-theorem wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
-by (rule acc_wfI) (rule all_accessible)
-
-theorem wf_mult: "wf r \<Longrightarrow> wf (mult r)"
-unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+lemma wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
+  by (rule acc_wfI) (rule all_accessible)
+
+lemma wf_mult: "wf r \<Longrightarrow> wf (mult r)"
+  unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+
+lemma wfP_multp: "wfP r \<Longrightarrow> wfP (multp r)"
+  unfolding multp_def wfP_def
+  by (simp add: wf_mult)
 
 
 subsubsection \<open>Closure-free presentation\<close>
@@ -2965,6 +2986,9 @@
   qed
 qed
 
+lemmas multp_implies_one_step =
+  mult_implies_one_step[of "{(x, y). r x y}" for r, folded multp_def transp_trans, simplified]
+
 lemma one_step_implies_mult:
   assumes
     "J \<noteq> {#}" and
@@ -2997,6 +3021,9 @@
   qed
 qed
 
+lemmas one_step_implies_multp =
+  one_step_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def, simplified]
+
 lemma subset_implies_mult:
   assumes sub: "A \<subset># B"
   shows "(A, B) \<in> mult r"
@@ -3009,8 +3036,10 @@
     by (rule one_step_implies_mult[of "B - A" "{#}" _ A, unfolded ApBmA, simplified])
 qed
 
-
-subsection \<open>The multiset extension is cancellative for multiset union\<close>
+lemmas subset_implies_multp = subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def]
+
+
+subsubsection \<open>The multiset extension is cancellative for multiset union\<close>
 
 lemma mult_cancel:
   assumes "trans s" and "irrefl s"
@@ -3045,10 +3074,18 @@
   thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
 qed
 
+lemmas multp_cancel =
+  mult_cancel[of "{(x, y). r x y}" for r,
+    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
 lemmas mult_cancel_add_mset =
   mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
 
-lemma mult_cancel_max:
+lemmas multp_cancel_add_mset =
+  mult_cancel_add_mset[of "{(x, y). r x y}" for r,
+    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
+lemma mult_cancel_max0:
   assumes "trans s" and "irrefl s"
   shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
 proof -
@@ -3056,6 +3093,112 @@
   thus ?thesis using mult_cancel[OF assms, of "X - X \<inter># Y"  "X \<inter># Y" "Y - X \<inter># Y"] by auto
 qed
 
+lemmas mult_cancel_max = mult_cancel_max0[simplified]
+
+lemmas multp_cancel_max =
+  mult_cancel_max[of "{(x, y). r x y}" for r,
+    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
+
+subsubsection \<open>Partial-order properties\<close>
+
+lemma mult1_lessE:
+  assumes "(N, M) \<in> mult1 {(a, b). r a b}" and "asymp r"
+  obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
+    "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
+proof -
+  from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
+    *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
+  moreover from * [of a] have "a \<notin># K"
+    using \<open>asymp r\<close> by (meson asymp.cases)
+  ultimately show thesis by (auto intro: that)
+qed
+
+lemma trans_mult: "trans r \<Longrightarrow> trans (mult r)"
+  by (simp add: mult_def)
+
+lemma transp_multp: "transp r \<Longrightarrow> transp (multp r)"
+  unfolding multp_def transp_trans_eq
+  by (fact trans_mult[of "{(x, y). r x y}" for r, folded transp_trans])
+
+lemma irrefl_mult:
+  assumes "trans r" "irrefl r"
+  shows "irrefl (mult r)"
+proof (intro irreflI notI)
+  fix M
+  assume "(M, M) \<in> mult r"
+  then obtain I J K where "M = I + J" and "M = I + K"
+    and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> r)"
+    using mult_implies_one_step[OF \<open>trans r\<close>] by blast
+  then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. (k, j) \<in> r" by auto
+  have "finite (set_mset K)" by simp
+  hence "set_mset K = {}"
+    using **
+  proof (induction rule: finite_induct)
+    case empty
+    thus ?case by simp
+  next
+    case (insert x F)
+    have False
+      using \<open>irrefl r\<close>[unfolded irrefl_def, rule_format]
+      using \<open>trans r\<close>[THEN transD]
+      by (metis equals0D insert.IH insert.prems insertE insertI1 insertI2)
+    thus ?case ..
+  qed
+  with * show False by simp
+qed
+
+lemmas irreflp_multp =
+  irrefl_mult[of "{(x, y). r x y}" for r,
+    folded transp_trans_eq irreflp_irrefl_eq, simplified, folded multp_def]
+
+instantiation multiset :: (preorder) order begin
+
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+  where "M < N \<longleftrightarrow> multp (<) M N"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+  where "less_eq_multiset M N \<longleftrightarrow> M < N \<or> M = N"
+
+instance
+proof intro_classes
+  fix M N :: "'a multiset"
+  show "(M < N) = (M \<le> N \<and> \<not> N \<le> M)"
+    unfolding less_eq_multiset_def less_multiset_def
+    by (metis irreflp_def irreflp_less irreflp_multp transpE transp_less transp_multp)
+next
+  fix M :: "'a multiset"
+  show "M \<le> M"
+    unfolding less_eq_multiset_def
+    by simp
+next
+  fix M1 M2 M3 :: "'a multiset"
+  show "M1 \<le> M2 \<Longrightarrow> M2 \<le> M3 \<Longrightarrow> M1 \<le> M3"
+    unfolding less_eq_multiset_def less_multiset_def
+    using transp_multp[OF transp_less, THEN transpD]
+    by blast
+next
+  fix M N :: "'a multiset"
+  show "M \<le> N \<Longrightarrow> N \<le> M \<Longrightarrow> M = N"
+    unfolding less_eq_multiset_def less_multiset_def
+    using transp_multp[OF transp_less, THEN transpD]
+    using irreflp_multp[OF transp_less irreflp_less, unfolded irreflp_def, rule_format]
+    by blast
+qed
+
+end
+
+lemma mset_le_irrefl [elim!]:
+  fixes M :: "'a::preorder multiset"
+  shows "M < M \<Longrightarrow> R"
+  by simp
+
+lemma wfP_less_multiset[simp]:
+  assumes wfP_less: "wfP ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
+  shows "wfP ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
+  using wfP_multp[OF wfP_less] less_multiset_def
+  by (metis wfPUNIVI wfP_induct)
+
 
 subsection \<open>Quasi-executable version of the multiset extension\<close>
 
@@ -3063,22 +3206,22 @@
   Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are
   executable whenever the given predicate \<open>P\<close> is. Together with the standard
   code equations for \<open>(\<inter>#\<close>) and \<open>(-\<close>) this should yield quadratic
-  (with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>.
+  (with respect to calls to \<open>P\<close>) implementations of \<open>multp_code\<close> and \<open>multeqp_code\<close>.
 \<close>
 
-definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  "multp P N M =
+definition multp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "multp_code P N M =
     (let Z = M \<inter># N; X = M - Z in
     X \<noteq> {#} \<and> (let Y = N - Z in (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x)))"
 
-definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  "multeqp P N M =
+definition multeqp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "multeqp_code P N M =
     (let Z = M \<inter># N; X = M - Z; Y = N - Z in
     (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"
 
-lemma multp_iff:
+lemma multp_code_iff_mult:
   assumes "irrefl R" and "trans R" and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
-  shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
+  shows "multp_code P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
 proof -
   have *: "M \<inter># N + (N - M \<inter># N) = N" "M \<inter># N + (M - M \<inter># N) = M"
     "(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp flip: count_inject)
@@ -3086,87 +3229,40 @@
   proof
     assume ?L thus ?R
       using one_step_implies_mult[of "M - M \<inter># N" "N - M \<inter># N" R "M \<inter># N"] *
-      by (auto simp: multp_def Let_def)
+      by (auto simp: multp_code_def Let_def)
   next
     { fix I J K :: "'a multiset" assume "(I + J) \<inter># (I + K) = {#}"
       then have "I = {#}" by (metis inter_union_distrib_right union_eq_empty)
     } note [dest!] = this
     assume ?R thus ?L
       using mult_implies_one_step[OF assms(2), of "N - M \<inter># N" "M - M \<inter># N"]
-        mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_def)
+        mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_code_def)
   qed
 qed
 
-lemma multeqp_iff:
+lemma multp_code_eq_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multp_code r = multp r"
+  using multp_code_iff_mult[of "{(x, y). r x y}" r for r,
+    folded irreflp_irrefl_eq transp_trans multp_def, simplified]
+  by blast
+
+lemma multeqp_code_iff_reflcl_mult:
   assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
-  shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
+  shows "multeqp_code P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
 proof -
   { assume "N \<noteq> M" "M - M \<inter># N = {#}"
     then obtain y where "count N y \<noteq> count M y" by (auto simp flip: count_inject)
     then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
       by (auto simp flip: count_inject dest!: le_neq_implies_less fun_cong[of _ _ y])
   }
-  then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
-    by (auto simp: multeqp_def multp_def Let_def in_diff_count)
-  thus ?thesis using multp_iff[OF assms] by simp
-qed
-
-
-subsubsection \<open>Partial-order properties\<close>
-
-lemma (in preorder) mult1_lessE:
-  assumes "(N, M) \<in> mult1 {(a, b). a < b}"
-  obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
-    "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
-proof -
-  from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
-    *: "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
-  moreover from * [of a] have "a \<notin># K" by auto
-  ultimately show thesis by (auto intro: that)
+  then have "multeqp_code P N M \<longleftrightarrow> multp_code P N M \<or> N = M"
+    by (auto simp: multeqp_code_def multp_code_def Let_def in_diff_count)
+  thus ?thesis using multp_code_iff_mult[OF assms] by simp
 qed
 
-instantiation multiset :: (preorder) order
-begin
-
-definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
-  where "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
-  where "less_eq_multiset M' M \<longleftrightarrow> M' < M \<or> M' = M"
-
-instance
-proof -
-  have irrefl: "\<not> M < M" for M :: "'a multiset"
-  proof
-    assume "M < M"
-    then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
-    have "trans {(x'::'a, x). x' < x}"
-      by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
-    moreover note MM
-    ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
-      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
-      by (rule mult_implies_one_step)
-    then obtain I J K where "M = I + J" and "M = I + K"
-      and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
-    then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
-    have "finite (set_mset K)" by simp
-    moreover note **
-    ultimately have "set_mset K = {}"
-      by (induct rule: finite_induct) (auto intro: order_less_trans)
-    with * show False by simp
-  qed
-  have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
-    unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-  show "OFCLASS('a multiset, order_class)"
-    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
-qed
-
-end
-
-lemma mset_le_irrefl [elim!]:
-  fixes M :: "'a::preorder multiset"
-  shows "M < M \<Longrightarrow> R"
-  by simp
+lemma multeqp_code_eq_reflclp_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multeqp_code r = (multp r)\<^sup>=\<^sup>="
+  using multeqp_code_iff_reflcl_mult[of "{(x, y). r x y}" r for r,
+    folded irreflp_irrefl_eq transp_trans, simplified, folded multp_def]
+  by blast
 
 
 subsubsection \<open>Monotonicity of multiset union\<close>
@@ -3175,7 +3271,7 @@
   by (force simp: mult1_def)
 
 lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
-apply (unfold less_multiset_def mult_def)
+apply (unfold less_multiset_def multp_def mult_def)
 apply (erule trancl_induct)
  apply (blast intro: mult1_union)
 apply (blast intro: mult1_union trancl_trans)
diff -r 98d2b3375258 -r e8935405f082 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Sat Dec 04 12:38:51 2021 +0100
@@ -11,6 +11,135 @@
 
 subsection \<open>Alternative Characterizations\<close>
 
+subsubsection \<open>The Dershowitz--Manna Ordering\<close>
+
+definition multp\<^sub>D\<^sub>M where
+  "multp\<^sub>D\<^sub>M r M N \<longleftrightarrow>
+   (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)))"
+
+lemma multp\<^sub>D\<^sub>M_imp_multp:
+  "multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N"
+proof -
+  assume "multp\<^sub>D\<^sub>M r M N"
+  then obtain X Y where
+    "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)"
+    unfolding multp\<^sub>D\<^sub>M_def by blast
+  then have "multp r (N - X + Y) (N - X + X)"
+    by (intro one_step_implies_multp) (auto simp: Bex_def trans_def)
+  with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "multp r M N"
+    by (metis subset_mset.diff_add)
+qed
+
+subsubsection \<open>The Huet--Oppen Ordering\<close>
+
+definition multp\<^sub>H\<^sub>O where
+  "multp\<^sub>H\<^sub>O r M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. r y x \<and> count M x < count N x))"
+
+lemma multp_imp_multp\<^sub>H\<^sub>O:
+  assumes "asymp r" and "transp r"
+  shows "multp r M N \<Longrightarrow> multp\<^sub>H\<^sub>O r M N"
+  unfolding multp_def mult_def
+proof (induction rule: trancl_induct)
+  case (base P)
+  then show ?case
+    using \<open>asymp r\<close>
+    by (auto elim!: mult1_lessE simp: count_eq_zero_iff multp\<^sub>H\<^sub>O_def split: if_splits
+        dest!: Suc_lessD)
+next
+  case (step N P)
+  from step(3) have "M \<noteq> N" and
+    **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x. r y x \<and> count M x < count N x)"
+    by (simp_all add: multp\<^sub>H\<^sub>O_def)
+  from step(2) obtain M0 a K where
+    *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
+    using \<open>asymp r\<close> by (auto elim: mult1_lessE)
+  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P"
+    using *(4) \<open>asymp r\<close>
+    by (metis asymp.cases add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
+        count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
+  moreover
+  { assume "count P a \<le> count M a"
+    with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
+      by (auto simp add: not_in_iff)
+      with ** obtain z where z: "r a z" "count M z < count N z"
+        by blast
+      with * have "count N z \<le> count P z"
+        using \<open>asymp r\<close>
+        by (metis add_diff_cancel_left' add_mset_add_single asymp.cases diff_diff_add_mset
+            diff_single_trivial in_diff_count not_le_imp_less)
+      with z have "\<exists>z. r a z \<and> count M z < count P z" by auto
+  } note count_a = this
+  { fix y
+    assume count_y: "count P y < count M y"
+    have "\<exists>x. r y x \<and> count M x < count P x"
+    proof (cases "y = a")
+      case True
+      with count_y count_a show ?thesis by auto
+    next
+      case False
+      show ?thesis
+      proof (cases "y \<in># K")
+        case True
+        with *(4) have "r y a" by simp
+        then show ?thesis
+          by (cases "count P a \<le> count M a") (auto dest: count_a intro: \<open>transp r\<close>[THEN transpD])
+      next
+        case False
+        with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
+          by (simp add: not_in_iff)
+        with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto
+        show ?thesis
+        proof (cases "z \<in># K")
+          case True
+          with *(4) have "r z a" by simp
+          with z(1) show ?thesis
+            by (cases "count P a \<le> count M a") (auto dest!: count_a intro: \<open>transp r\<close>[THEN transpD])
+        next
+          case False
+          with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
+            by (auto simp add: not_in_iff)
+          with z show ?thesis by auto
+        qed
+      qed
+    qed
+  }
+  ultimately show ?case unfolding multp\<^sub>H\<^sub>O_def by blast
+qed
+
+lemma multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M: "multp\<^sub>H\<^sub>O r M N \<Longrightarrow> multp\<^sub>D\<^sub>M r M N"
+unfolding multp\<^sub>D\<^sub>M_def
+proof (intro iffI exI conjI)
+  assume "multp\<^sub>H\<^sub>O r M N"
+  then obtain z where z: "count M z < count N z"
+    unfolding multp\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
+  define X where "X = N - M"
+  define Y where "Y = M - N"
+  from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
+  from z show "X \<subseteq># N" unfolding X_def by auto
+  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
+  show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)"
+  proof (intro allI impI)
+    fix k
+    assume "k \<in># Y"
+    then have "count N k < count M k" unfolding Y_def
+      by (auto simp add: in_diff_count)
+    with \<open>multp\<^sub>H\<^sub>O r M N\<close> obtain a where "r k a" and "count M a < count N a"
+      unfolding multp\<^sub>H\<^sub>O_def by blast
+    then show "\<exists>a. a \<in># X \<and> r k a" unfolding X_def
+      by (auto simp add: in_diff_count)
+  qed
+qed
+
+lemma multp_eq_multp\<^sub>D\<^sub>M: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>D\<^sub>M r"
+  using multp\<^sub>D\<^sub>M_imp_multp multp_imp_multp\<^sub>H\<^sub>O[THEN multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M]
+  by blast
+
+lemma multp_eq_multp\<^sub>H\<^sub>O: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>H\<^sub>O r"
+  using multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M[THEN multp\<^sub>D\<^sub>M_imp_multp] multp_imp_multp\<^sub>H\<^sub>O
+  by blast
+
+subsubsection \<open>Properties of Preorders\<close>
+
 context preorder
 begin
 
@@ -59,107 +188,29 @@
 
 lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
   "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
-proof (unfold mult_def, induct rule: trancl_induct)
-  case (base P)
-  then show ?case
-    by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD)
-next
-  case (step N P)
-  from step(3) have "M \<noteq> N" and
-    **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
-    by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
-  from step(2) obtain M0 a K where
-    *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
-    by (blast elim: mult1_lessE)
-  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
-  moreover
-  { assume "count P a \<le> count M a"
-    with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
-      by (auto simp add: not_in_iff)
-      with ** obtain z where z: "z > a" "count M z < count N z"
-        by blast
-      with * have "count N z \<le> count P z" 
-        by (auto elim: less_asym intro: count_inI)
-      with z have "\<exists>z > a. count M z < count P z" by auto
-  } note count_a = this
-  { fix y
-    assume count_y: "count P y < count M y"
-    have "\<exists>x>y. count M x < count P x"
-    proof (cases "y = a")
-      case True
-      with count_y count_a show ?thesis by auto
-    next
-      case False
-      show ?thesis
-      proof (cases "y \<in># K")
-        case True
-        with *(4) have "y < a" by simp
-        then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
-      next
-        case False
-        with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
-          by (simp add: not_in_iff)
-        with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto
-        show ?thesis
-        proof (cases "z \<in># K")
-          case True
-          with *(4) have "z < a" by simp
-          with z(1) show ?thesis
-            by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
-        next
-          case False
-          with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
-            by (auto simp add: not_in_iff)
-          with z show ?thesis by auto
-        qed
-      qed
-    qed
-  }
-  ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast
-qed
+  unfolding multp_def[of "(<)", symmetric]
+  using multp_imp_multp\<^sub>H\<^sub>O[of "(<)"]
+  by (simp add: less_multiset\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_def)
 
 lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
   "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
-proof -
-  assume "less_multiset\<^sub>D\<^sub>M M N"
-  then obtain X Y where
-    "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
-    unfolding less_multiset\<^sub>D\<^sub>M_def by blast
-  then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
-    by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
-  with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}"
-    by (metis subset_mset.diff_add)
-qed
+  unfolding multp_def[of "(<)", symmetric]
+  by (rule multp\<^sub>D\<^sub>M_imp_multp[of "(<)" M N]) (simp add: less_multiset\<^sub>D\<^sub>M_def multp\<^sub>D\<^sub>M_def)
 
 lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N"
-unfolding less_multiset\<^sub>D\<^sub>M_def
-proof (intro iffI exI conjI)
-  assume "less_multiset\<^sub>H\<^sub>O M N"
-  then obtain z where z: "count M z < count N z"
-    unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
-  define X where "X = N - M"
-  define Y where "Y = M - N"
-  from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
-  from z show "X \<subseteq># N" unfolding X_def by auto
-  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
-  show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
-  proof (intro allI impI)
-    fix k
-    assume "k \<in># Y"
-    then have "count N k < count M k" unfolding Y_def
-      by (auto simp add: in_diff_count)
-    with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
-      unfolding less_multiset\<^sub>H\<^sub>O_def by blast
-    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def
-      by (auto simp add: in_diff_count)
-  qed
-qed
+  unfolding less_multiset\<^sub>D\<^sub>M_def less_multiset\<^sub>H\<^sub>O_def
+  unfolding multp\<^sub>D\<^sub>M_def[symmetric] multp\<^sub>H\<^sub>O_def[symmetric]
+  by (rule multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M)
 
 lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N"
-  by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
+  unfolding multp_def[of "(<)", symmetric]
+  using multp_eq_multp\<^sub>D\<^sub>M[of "(<)", simplified]
+  by (simp add: multp\<^sub>D\<^sub>M_def less_multiset\<^sub>D\<^sub>M_def)
 
 lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
-  by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
+  unfolding multp_def[of "(<)", symmetric]
+  using multp_eq_multp\<^sub>H\<^sub>O[of "(<)", simplified]
+  by (simp add: multp\<^sub>H\<^sub>O_def less_multiset\<^sub>H\<^sub>O_def)
 
 lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
 lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
@@ -167,10 +218,15 @@
 end
 
 lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
-  unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
+  unfolding less_multiset_def multp_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
 
-lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
-lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
+lemma less_multiset\<^sub>D\<^sub>M:
+  "M < N \<longleftrightarrow> (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
+  by (rule mult\<^sub>D\<^sub>M[folded multp_def less_multiset_def])
+
+lemma less_multiset\<^sub>H\<^sub>O:
+  "M < N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x>y. count M x < count N x))"
+  by (rule mult\<^sub>H\<^sub>O[folded multp_def less_multiset_def])
 
 lemma subset_eq_imp_le_multiset:
   shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
@@ -198,7 +254,7 @@
 
 (* FIXME: "le" should be "less" in this and other names *)
 lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
-  using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
+  using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M by blast
 
 (* FIXME: "le" should be "less" in this and other names *)
 lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
@@ -381,9 +437,9 @@
 begin
 
 lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
-  unfolding less_multiset_def by (auto intro: wf_mult wf)
+  unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)
 
-instance by standard (metis less_multiset_def wf wf_def wf_mult)
+instance by standard (metis less_multiset_def multp_def wf wf_def wf_mult)
 
 end
 
diff -r 98d2b3375258 -r e8935405f082 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/List.thy	Sat Dec 04 12:38:51 2021 +0100
@@ -4238,6 +4238,8 @@
   case (Cons x xs) thus ?case by (fastforce split: if_splits)
 qed
 
+lemmas find_None_iff2 = find_None_iff[THEN eq_iff_swap]
+
 lemma find_Some_iff:
   "List.find P xs = Some x \<longleftrightarrow>
   (\<exists>i<length xs. P (xs!i) \<and> x = xs!i \<and> (\<forall>j<i. \<not> P (xs!j)))"
@@ -4249,6 +4251,8 @@
     using diff_Suc_1[unfolded One_nat_def] less_Suc_eq_0_disj by fastforce
 qed
 
+lemmas find_Some_iff2 = find_Some_iff[THEN eq_iff_swap]
+
 lemma find_cong[fundef_cong]:
   assumes "xs = ys" and "\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x"
   shows "List.find P xs = List.find Q ys"
diff -r 98d2b3375258 -r e8935405f082 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Map.thy	Sat Dec 04 12:38:51 2021 +0100
@@ -667,6 +667,10 @@
 lemma fun_upd_None_if_notin_dom[simp]: "k \<notin> dom m \<Longrightarrow> m(k := None) = m"
   by auto
 
+lemma ran_map_upd_Some:
+  "\<lbrakk> m x = Some y; inj_on m (dom m); z \<notin> ran m \<rbrakk> \<Longrightarrow> ran(m(x := Some z)) = ran m - {y} \<union> {z}"
+by(force simp add: ran_def domI inj_onD)
+
 lemma ran_map_add:
   assumes "dom m1 \<inter> dom m2 = {}"
   shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
diff -r 98d2b3375258 -r e8935405f082 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Relation.thy	Sat Dec 04 12:38:51 2021 +0100
@@ -241,6 +241,11 @@
 lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
   by (auto simp add: irrefl_def)
 
+lemma (in preorder) irreflp_less[simp]: "irreflp (<)"
+  by (simp add: irreflpI)
+
+lemma (in preorder) irreflp_greater[simp]: "irreflp (>)"
+  by (simp add: irreflpI)
 
 subsubsection \<open>Asymmetry\<close>
 
@@ -259,6 +264,17 @@
 lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
   by (blast intro: asymI dest: asymD)
 
+context preorder begin
+
+lemma asymp_less[simp]: "asymp (<)"
+  by (auto intro: asympI dual_order.asym)
+
+lemma asymp_greater[simp]: "asymp (>)"
+  by (auto intro: asympI dual_order.asym)
+
+end
+
+
 subsubsection \<open>Symmetry\<close>
 
 definition sym :: "'a rel \<Rightarrow> bool"
diff -r 98d2b3375258 -r e8935405f082 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/HOL/Wellfounded.thy	Sat Dec 04 12:38:51 2021 +0100
@@ -79,6 +79,9 @@
 lemma (in wellorder) wf: "wf {(x, y). x < y}"
   unfolding wf_def by (blast intro: less_induct)
 
+lemma (in wellorder) wfP_less[simp]: "wfP (<)"
+  by (simp add: wf wfP_def)
+
 
 subsection \<open>Basic Results\<close>
 
diff -r 98d2b3375258 -r e8935405f082 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Pure/Admin/build_release.scala	Sat Dec 04 12:38:51 2021 +0100
@@ -837,6 +837,9 @@
 
             val other_isabelle = context.other_isabelle(tmp_dir)
 
+            Isabelle_System.make_directory(other_isabelle.etc)
+            File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n")
+
             other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
               " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
               " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
diff -r 98d2b3375258 -r e8935405f082 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Dec 04 12:38:51 2021 +0100
@@ -204,7 +204,7 @@
     profiles: List[Profile] = default_profiles,
     only_sessions: Set[String] = Set.empty,
     ml_statistics: Boolean = false,
-    ml_statistics_domain: String => Boolean = (key: String) => true,
+    ml_statistics_domain: String => Boolean = _ => true,
     verbose: Boolean = false): Data =
   {
     val date = Date.now()
@@ -377,7 +377,7 @@
           List(HTML.description(
             List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
         HTML.par(
-          List(HTML.itemize(data.entries.map({ case data_entry =>
+          List(HTML.itemize(data.entries.map(data_entry =>
             List(
               HTML.link(clean_name(data_entry.name) + "/index.html",
                 HTML.text(data_entry.name))) :::
@@ -388,7 +388,7 @@
                 List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
                 List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
             })
-          }))))))
+          ))))))
 
     for (data_entry <- data.entries) {
       val data_name = data_entry.name
@@ -423,10 +423,10 @@
                       entry.ml_timing.elapsed.minutes.toString,
                       entry.ml_timing.resources.minutes.toString,
                       entry.maximum_code.toString,
-                      entry.maximum_code.toString,
+                      entry.average_code.toString,
+                      entry.maximum_stack.toString,
                       entry.average_stack.toString,
-                      entry.maximum_stack.toString,
-                      entry.average_heap.toString,
+                      entry.maximum_heap.toString,
                       entry.average_heap.toString,
                       entry.stored_heap.toString).mkString(" "))))
 
@@ -608,7 +608,7 @@
         "l:" -> (arg => options = options + ("build_log_history=" + arg)),
         "o:" -> (arg => options = options + arg),
         "s:" -> (arg =>
-          space_explode('x', arg).map(Value.Int.parse(_)) match {
+          space_explode('x', arg).map(Value.Int.parse) match {
             case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
             case _ => error("Error bad PNG image size: " + quote(arg))
           }),
diff -r 98d2b3375258 -r e8935405f082 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Dec 04 12:38:51 2021 +0100
@@ -314,7 +314,7 @@
   {
     List(
       List(Remote_Build("Linux A", "augsburg1",
-          options = "-m32 -B -M1x2,2,4" +
+          options = "-m32 -B -M4" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
             " -e ISABELLE_GHC_SETUP=true" +
             " -e ISABELLE_MLTON=mlton" +
diff -r 98d2b3375258 -r e8935405f082 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sat Dec 04 12:38:51 2021 +0100
@@ -194,7 +194,7 @@
   val empty: ML_Statistics = apply(Nil)
 
   def apply(ml_statistics0: List[Properties.T], heading: String = "",
-    domain: String => Boolean = (key: String) => true): ML_Statistics =
+    domain: String => Boolean = _ => true): ML_Statistics =
   {
     require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
 
@@ -260,6 +260,11 @@
   val time_start: Double,
   val duration: Double)
 {
+  override def toString: String =
+    if (content.isEmpty) "ML_Statistics.empty"
+    else "ML_Statistics(length = " + content.length + ", fields = " + fields.size + ")"
+
+
   /* content */
 
   def maximum(field: String): Double =
@@ -286,7 +291,7 @@
 
   def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
   {
-    data.removeAllSeries
+    data.removeAllSeries()
     for (field <- selected_fields) {
       val series = new XYSeries(field)
       content.foreach(entry => series.add(entry.time, entry.get(field)))
diff -r 98d2b3375258 -r e8935405f082 src/Tools/VSCode/extension/README.md
--- a/src/Tools/VSCode/extension/README.md	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Tools/VSCode/extension/README.md	Sat Dec 04 12:38:51 2021 +0100
@@ -1,14 +1,15 @@
 # Isabelle Prover IDE support
 
 This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
-requires Isabelle2021-1.
+requires a suitable repository version of Isabelle.
 
 The implementation is centered around the VSCode Language Server protocol, but
 with many add-ons that are specific to VSCode and Isabelle/PIDE.
 
 See also:
 
-  * <https://isabelle.in.tum.de/website-Isabelle2021-1>
+  * <https://isabelle.sketis.net/repos/isabelle/file/tip/src/Tools/VSCode>
+  * <https://github.com/Microsoft/language-server-protocol>
 
 
 ## Screenshot
@@ -57,8 +58,8 @@
 
 ### Isabelle/VSCode Installation
 
-  * Download Isabelle2021-1 from <https://isabelle.in.tum.de/website-Isabelle2021-1>
-  or any of its mirror sites.
+  * Download a recent Isabelle development snapshot from
+    <https://isabelle.sketis.net/devel/release_snapshot>
 
   * Unpack and run the main Isabelle/jEdit application as usual, to ensure that
   the logic image is built properly and Isabelle works as expected.
@@ -88,17 +89,17 @@
 
       + Linux:
         ```
-        "isabelle.home": "/home/makarius/Isabelle2021-1"
+        "isabelle.home": "/home/makarius/Isabelle"
         ```
 
       + Mac OS X:
         ```
-        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2021-1"
+        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
         ```
 
       + Windows:
         ```
-        "isabelle.home": "C:\\Users\\makarius\\Isabelle2021-1"
+        "isabelle.home": "C:\\Users\\makarius\\Isabelle"
         ```
 
   * Restart the VSCode application to ensure that all extensions are properly
diff -r 98d2b3375258 -r e8935405f082 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Tools/VSCode/extension/package.json	Sat Dec 04 12:38:51 2021 +0100
@@ -1,6 +1,6 @@
 {
-    "name": "Isabelle2021-1",
-    "displayName": "Isabelle2021-1",
+    "name": "Isabelle",
+    "displayName": "Isabelle",
     "description": "Isabelle Prover IDE",
     "keywords": [
         "theorem prover",