# HG changeset patch
# User wenzelm
# Date 1467746601 -7200
# Node ID a528d24826c54e2b0f247b77fdb443ff21e66049
# Parent  c22928719e198a58fd796f6b0aee6262119d9ed4# Parent  ae07cd27ebf1886877b950315be77d1247613edd
merged

diff -r ae07cd27ebf1 -r a528d24826c5 NEWS
--- a/NEWS	Tue Jul 05 20:51:02 2016 +0200
+++ b/NEWS	Tue Jul 05 21:23:21 2016 +0200
@@ -311,6 +311,43 @@
   Some functions have been renamed:
     ms_lesseq_impl -> subset_eq_mset_impl
 
+* Multisets are now ordered with the multiset ordering
+    #\<subseteq># ~> \<le>
+    #\<subset># ~> <
+    le_multiset ~> less_eq_multiset
+    less_multiset ~> le_multiset
+INCOMPATIBILITY
+
+* The prefix multiset_order has been discontinued: the theorems can be directly
+accessed.
+INCOMPATILBITY
+
+* Some theorems about the multiset ordering have been renamed:
+    le_multiset_def ~> less_eq_multiset_def
+    less_multiset_def ~> le_multiset_def
+    less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
+    mult_less_not_refl ~> mset_le_not_refl
+    mult_less_trans ~> mset_le_trans
+    mult_less_not_sym ~> mset_le_not_sym
+    mult_less_asym ~> mset_le_asym
+    mult_less_irrefl ~> mset_le_irrefl
+    union_less_mono2{,1,2} ~> union_le_mono2{,1,2}
+
+    le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
+    le_multiset_total ~> less_eq_multiset_total
+    less_multiset_right_total ~> subset_eq_imp_le_multiset
+    le_multiset_empty_left ~> less_eq_multiset_empty_left
+    le_multiset_empty_right ~> less_eq_multiset_empty_right
+    less_multiset_empty_right ~> le_multiset_empty_left
+    less_multiset_empty_left ~> le_multiset_empty_right
+    union_less_diff_plus ~> union_le_diff_plus
+    ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
+    less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
+    le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
+    less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff
+    less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
+INCOMPATIBILITY
+
 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
 INCOMPATIBILITY.
 
diff -r ae07cd27ebf1 -r a528d24826c5 src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/Doc/Locales/Examples3.thy	Tue Jul 05 21:23:21 2016 +0200
@@ -91,8 +91,8 @@
 \begin{tabular}{l}
   @{thm [source] int.less_def} from locale @{text partial_order}: \\
   \quad @{thm int.less_def} \\
-  @{thm [source] int.meet_left} from locale @{text lattice}: \\
-  \quad @{thm int.meet_left} \\
+  @{thm [source] int.ex_sup} from locale @{text lattice}: \\
+  \quad @{thm int.ex_sup} \\
   @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
   \quad @{thm int.join_distr} \\
   @{thm [source] int.less_total} from locale @{text total_order}: \\
@@ -408,7 +408,7 @@
     assumes non_neg: "0 \<le> n"
 
 text \<open>It is again convenient to make the interpretation in an
-  incremental fashion, first for order preserving maps, the for
+  incremental fashion, first for order preserving maps, then for
   lattice endomorphisms.\<close>
 
   sublocale non_negative \<subseteq>
diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Jul 05 21:23:21 2016 +0200
@@ -2500,21 +2500,20 @@
   ultimately show thesis by (auto intro: that)
 qed
 
-definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subset>#" 50)
-  where "M' #\<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subseteq>#" 50)
-  where "M' #\<subseteq># M \<longleftrightarrow> M' #\<subset># M \<or> M' = M"
-
-notation (ASCII)
-  less_multiset (infix "#<#" 50) and
-  le_multiset (infix "#<=#" 50)
-
-interpretation multiset_order: order le_multiset less_multiset
+instantiation multiset :: (order) 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 #\<subset># M" for M :: "'a multiset"
+  have irrefl: "\<not> M < M" for M :: "'a multiset"
   proof
-    assume "M #\<subset># M"
+    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 (rule transI) simp
@@ -2531,15 +2530,16 @@
       by (induct rule: finite_induct) (auto intro: order_less_trans)
     with * show False by simp
   qed
-  have trans: "K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N" for K M N :: "'a multiset"
+  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 "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
-    by standard (auto simp add: le_multiset_def irrefl dest: trans)
-qed \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
-
-lemma mult_less_irrefl [elim!]:
+  show "OFCLASS('a multiset, order_class)"
+    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
+qed
+end \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
+
+lemma mset_le_irrefl [elim!]:
   fixes M :: "'a::order multiset"
-  shows "M #\<subset># M \<Longrightarrow> R"
+  shows "M < M \<Longrightarrow> R"
   by simp
 
 
@@ -2553,27 +2553,29 @@
 apply (simp add: add.assoc)
 done
 
-lemma union_less_mono2: "B #\<subset># D \<Longrightarrow> C + B #\<subset># C + (D::'a::order multiset)"
+lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::order multiset)"
 apply (unfold less_multiset_def mult_def)
 apply (erule trancl_induct)
  apply (blast intro: mult1_union)
 apply (blast intro: mult1_union trancl_trans)
 done
 
-lemma union_less_mono1: "B #\<subset># D \<Longrightarrow> B + C #\<subset># D + (C::'a::order multiset)"
+lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::order multiset)"
 apply (subst add.commute [of B C])
 apply (subst add.commute [of D C])
-apply (erule union_less_mono2)
+apply (erule union_le_mono2)
 done
 
 lemma union_less_mono:
   fixes A B C D :: "'a::order multiset"
-  shows "A #\<subset># C \<Longrightarrow> B #\<subset># D \<Longrightarrow> A + B #\<subset># C + D"
-  by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
-
-interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
-  by standard (auto simp add: le_multiset_def intro: union_less_mono2)
-
+  shows "A < C \<Longrightarrow> B < D \<Longrightarrow> A + B < C + D"
+  by (blast intro!: union_le_mono1 union_le_mono2 less_trans)
+
+instantiation multiset :: (order) ordered_ab_semigroup_add
+begin
+instance
+  by standard (auto simp add: less_eq_multiset_def intro: union_le_mono2)
+end
 
 subsubsection \<open>Termination proofs with multiset orders\<close>
 
@@ -2767,17 +2769,17 @@
   multiset_inter_assoc
   multiset_inter_left_commute
 
-lemma mult_less_not_refl: "\<not> M #\<subset># (M::'a::order multiset)"
-  by (fact multiset_order.less_irrefl)
-
-lemma mult_less_trans: "K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># (N::'a::order multiset)"
-  by (fact multiset_order.less_trans)
-
-lemma mult_less_not_sym: "M #\<subset># N \<Longrightarrow> \<not> N #\<subset># (M::'a::order multiset)"
-  by (fact multiset_order.less_not_sym)
-
-lemma mult_less_asym: "M #\<subset># N \<Longrightarrow> (\<not> P \<Longrightarrow> N #\<subset># (M::'a::order multiset)) \<Longrightarrow> P"
-  by (fact multiset_order.less_asym)
+lemma mset_le_not_refl: "\<not> M < (M::'a::order multiset)"
+  by (fact less_irrefl)
+
+lemma mset_le_trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < (N::'a::order multiset)"
+  by (fact less_trans)
+
+lemma mset_le_not_sym: "M < N \<Longrightarrow> \<not> N < (M::'a::order multiset)"
+  by (fact less_not_sym)
+
+lemma mset_le_asym: "M < N \<Longrightarrow> (\<not> P \<Longrightarrow> N < (M::'a::order multiset)) \<Longrightarrow> P"
+  by (fact less_asym)
 
 declaration \<open>
   let
@@ -2951,8 +2953,8 @@
 qed
 
 text \<open>
-  Exercise for the casual reader: add implementations for @{const le_multiset}
-  and @{const less_multiset} (multiset order).
+  Exercise for the casual reader: add implementations for @{term "op \<le>"}
+  and @{term "op <"} (multiset order).
 \<close>
 
 text \<open>Quickcheck generators\<close>
diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Tue Jul 05 21:23:21 2016 +0200
@@ -62,7 +62,7 @@
   have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
     unfolding mult_def by (blast intro: trancl_trans)
   show "class.order ?le ?less"
-    by standard (auto simp add: le_multiset_def irrefl dest: trans)
+    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
 qed
 
 text \<open>The Dershowitz--Manna ordering:\<close>
@@ -209,88 +209,88 @@
 end
 
 lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
-  "M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+  "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 ..
 
 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 le_multiset\<^sub>H\<^sub>O:
+lemma less_eq_multiset\<^sub>H\<^sub>O:
   fixes M N :: "('a :: linorder) multiset"
-  shows "M #\<subseteq># N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
-  by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
+  shows "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
+  by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
 
-lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M #\<subset># N}"
+lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M < N}"
   unfolding less_multiset_def by (auto intro: wf_mult wf)
 
 lemma order_multiset: "class.order
-  (le_multiset :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)
-  (less_multiset :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)"
+  (op \<le> :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)
+  (op < :: ('a :: order) multiset \<Rightarrow> ('a :: order) multiset \<Rightarrow> bool)"
   by unfold_locales
 
 lemma linorder_multiset: "class.linorder
-  (le_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)
-  (less_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)"
-  by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq)
+  (op \<le> :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)
+  (op < :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool)"
+  by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O less_eq_multiset_def not_less_iff_gr_or_eq)
 
 interpretation multiset_linorder: linorder
-  "le_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
-  "less_multiset :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
+  "op \<le> :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
+  "op < :: ('a :: linorder) multiset \<Rightarrow> ('a :: linorder) multiset \<Rightarrow> bool"
   by (rule linorder_multiset)
 
 interpretation multiset_wellorder: wellorder
-  "le_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
-  "less_multiset :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
+  "op \<le> :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
+  "op < :: ('a :: wellorder) multiset \<Rightarrow> ('a :: wellorder) multiset \<Rightarrow> bool"
   by unfold_locales (blast intro: wf_less_multiset [unfolded wf_def, simplified, rule_format])
 
-lemma le_multiset_total:
+lemma less_eq_multiset_total:
   fixes M N :: "('a :: linorder) multiset"
-  shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M"
+  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
   by (metis multiset_linorder.le_cases)
 
-lemma less_eq_imp_le_multiset:
+lemma subset_eq_imp_le_multiset:
   fixes M N :: "('a :: linorder) multiset"
-  shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
-  unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
+  shows "M \<le># N \<Longrightarrow> M \<le> N"
+  unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
   by (simp add: less_le_not_le subseteq_mset_def)
 
-lemma less_multiset_right_total:
+lemma le_multiset_right_total:
+  fixes M :: "('a :: linorder) multiset"
+  shows "M < M + {#undefined#}"
+  unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+
+lemma less_eq_multiset_empty_left[simp]:
   fixes M :: "('a :: linorder) multiset"
-  shows "M #\<subset># M + {#undefined#}"
-  unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+  shows "{#} \<le> M"
+  by (simp add: subset_eq_imp_le_multiset)
+
+lemma less_eq_multiset_empty_right[simp]:
+  fixes M :: "('a :: linorder) multiset"
+  shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
+  by (metis less_eq_multiset_empty_left antisym)
 
 lemma le_multiset_empty_left[simp]:
   fixes M :: "('a :: linorder) multiset"
-  shows "{#} #\<subseteq># M"
-  by (simp add: less_eq_imp_le_multiset)
+  shows "M \<noteq> {#} \<Longrightarrow> {#} < M"
+  by (simp add: less_multiset\<^sub>H\<^sub>O)
 
 lemma le_multiset_empty_right[simp]:
   fixes M :: "('a :: linorder) multiset"
-  shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}"
-  by (metis le_multiset_empty_left multiset_order.antisym)
-
-lemma less_multiset_empty_left[simp]:
-  fixes M :: "('a :: linorder) multiset"
-  shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M"
-  by (simp add: less_multiset\<^sub>H\<^sub>O)
-
-lemma less_multiset_empty_right[simp]:
-  fixes M :: "('a :: linorder) multiset"
-  shows "\<not> M #\<subset># {#}"
+  shows "\<not> M < {#}"
   using subset_eq_empty less_multiset\<^sub>D\<^sub>M by blast
 
 lemma
   fixes M N :: "('a :: linorder) multiset"
   shows
-    le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
-    le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
-  using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
+    less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
+    less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
+  using [[metis_verbose = false]] by (metis subset_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
 
 lemma
   fixes M N :: "('a :: linorder) multiset"
   shows
-    less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and
-    less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'"
+    le_multiset_plus_plus_left_iff[simp]: "M + N < M' + N \<longleftrightarrow> M < M'" and
+    le_multiset_plus_plus_right_iff[simp]: "M + N < M + N' \<longleftrightarrow> N < N'"
   unfolding less_multiset\<^sub>H\<^sub>O by auto
 
 lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
@@ -299,22 +299,22 @@
 lemma
   fixes M N :: "('a :: linorder) multiset"
   shows
-    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and
-    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N"
+    le_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
+    le_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M < M + N"
   using [[metis_verbose = false]]
-  by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
+  by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff
     add.commute)+
 
-lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
+lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
   unfolding less_multiset\<^sub>H\<^sub>O
   by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
-  
-lemma ex_gt_count_imp_less_multiset:
-  "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
+
+lemma ex_gt_count_imp_le_multiset:
+  "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
   unfolding less_multiset\<^sub>H\<^sub>O
   by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
 
-lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
-  by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
+lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
+  by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
 
 end
diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Jul 05 21:23:21 2016 +0200
@@ -1815,77 +1815,65 @@
   shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
+lemma Collect_closed_imp_pred_borel: "closed {x. P x} \<Longrightarrow> Measurable.pred borel P"
+  by (simp add: pred_def)
+
 (* Proof by Jeremy Avigad and Luke Serafin *)
+lemma isCont_borel_pred[measurable]:
+  fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
+  shows "Measurable.pred borel (isCont f)"
+proof (subst measurable_cong)
+  let ?I = "\<lambda>j. inverse(real (Suc j))"
+  show "isCont f x = (\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i)" for x
+    unfolding continuous_at_eps_delta
+  proof safe
+    fix i assume "\<forall>e>0. \<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
+    moreover have "0 < ?I i / 2"
+      by simp
+    ultimately obtain d where d: "0 < d" "\<And>y. dist x y < d \<Longrightarrow> dist (f y) (f x) < ?I i / 2"
+      by (metis dist_commute)
+    then obtain j where j: "?I j < d"
+      by (metis reals_Archimedean)
+
+    show "\<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
+    proof (safe intro!: exI[where x=j])
+      fix y z assume *: "dist x y < ?I j" "dist x z < ?I j"
+      have "dist (f y) (f z) \<le> dist (f y) (f x) + dist (f z) (f x)"
+        by (rule dist_triangle2)
+      also have "\<dots> < ?I i / 2 + ?I i / 2"
+        by (intro add_strict_mono d less_trans[OF _ j] *)
+      also have "\<dots> \<le> ?I i"
+        by (simp add: field_simps of_nat_Suc)
+      finally show "dist (f y) (f z) \<le> ?I i"
+        by simp
+    qed
+  next
+    fix e::real assume "0 < e"
+    then obtain n where n: "?I n < e"
+      by (metis reals_Archimedean)
+    assume "\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
+    from this[THEN spec, of "Suc n"]
+    obtain j where j: "\<And>y z. dist x y < ?I j \<Longrightarrow> dist x z < ?I j \<Longrightarrow> dist (f y) (f z) \<le> ?I (Suc n)"
+      by auto
+
+    show "\<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
+    proof (safe intro!: exI[of _ "?I j"])
+      fix y assume "dist y x < ?I j"
+      then have "dist (f y) (f x) \<le> ?I (Suc n)"
+        by (intro j) (auto simp: dist_commute)
+      also have "?I (Suc n) < ?I n"
+        by simp
+      also note n
+      finally show "dist (f y) (f x) < e" .
+    qed simp
+  qed
+qed (intro pred_intros_countable closed_Collect_all closed_Collect_le open_Collect_less
+           Collect_closed_imp_pred_borel closed_Collect_imp open_Collect_conj continuous_intros)
+
 lemma isCont_borel:
   fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
   shows "{x. isCont f x} \<in> sets borel"
-proof -
-  let ?I = "\<lambda>j. inverse(real (Suc j))"
-
-  { fix x
-    have "isCont f x = (\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i)"
-      unfolding continuous_at_eps_delta
-    proof safe
-      fix i assume "\<forall>e>0. \<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
-      moreover have "0 < ?I i / 2"
-        by simp
-      ultimately obtain d where d: "0 < d" "\<And>y. dist x y < d \<Longrightarrow> dist (f y) (f x) < ?I i / 2"
-        by (metis dist_commute)
-      then obtain j where j: "?I j < d"
-        by (metis reals_Archimedean)
-
-      show "\<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
-      proof (safe intro!: exI[where x=j])
-        fix y z assume *: "dist x y < ?I j" "dist x z < ?I j"
-        have "dist (f y) (f z) \<le> dist (f y) (f x) + dist (f z) (f x)"
-          by (rule dist_triangle2)
-        also have "\<dots> < ?I i / 2 + ?I i / 2"
-          by (intro add_strict_mono d less_trans[OF _ j] *)
-        also have "\<dots> \<le> ?I i"
-          by (simp add: field_simps of_nat_Suc)
-        finally show "dist (f y) (f z) \<le> ?I i"
-          by simp
-      qed
-    next
-      fix e::real assume "0 < e"
-      then obtain n where n: "?I n < e"
-        by (metis reals_Archimedean)
-      assume "\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
-      from this[THEN spec, of "Suc n"]
-      obtain j where j: "\<And>y z. dist x y < ?I j \<Longrightarrow> dist x z < ?I j \<Longrightarrow> dist (f y) (f z) \<le> ?I (Suc n)"
-        by auto
-
-      show "\<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
-      proof (safe intro!: exI[of _ "?I j"])
-        fix y assume "dist y x < ?I j"
-        then have "dist (f y) (f x) \<le> ?I (Suc n)"
-          by (intro j) (auto simp: dist_commute)
-        also have "?I (Suc n) < ?I n"
-          by simp
-        also note n
-        finally show "dist (f y) (f x) < e" .
-      qed simp
-    qed }
-  note * = this
-
-  have **: "\<And>e y. open {x. dist x y < e}"
-    using open_ball by (simp_all add: ball_def dist_commute)
-
-  have "{x\<in>space borel. isCont f x} \<in> sets borel"
-    unfolding *
-    apply (intro sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex)
-    apply (simp add: Collect_all_eq)
-    apply (intro borel_closed closed_INT ballI closed_Collect_imp open_Collect_conj **)
-    apply auto
-    done
-  then show ?thesis
-    by simp
-qed
-
-lemma isCont_borel_pred[measurable]:
-  fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
-  shows "Measurable.pred borel (isCont f)"
-  unfolding pred_def by (simp add: isCont_borel)
+  by simp
 
 lemma is_real_interval:
   assumes S: "is_interval S"
diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Probability/Levy.thy	Tue Jul 05 21:23:21 2016 +0200
@@ -219,64 +219,46 @@
   have "cdf M1 = cdf M2"
   proof (rule ext)
     fix x
-    from M1.cdf_is_right_cont [of x] have "(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)"
-      by (simp add: continuous_within)
-    from M2.cdf_is_right_cont [of x] have "(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)"
-      by (simp add: continuous_within)
+    let ?D = "\<lambda>x. \<bar>cdf M1 x - cdf M2 x\<bar>"
 
     { fix \<epsilon> :: real
       assume "\<epsilon> > 0"
-      from \<open>\<epsilon> > 0\<close> \<open>(cdf M1 \<longlongrightarrow> 0) at_bot\<close> \<open>(cdf M2 \<longlongrightarrow> 0) at_bot\<close>
-      have "eventually (\<lambda>y. \<bar>cdf M1 y\<bar> < \<epsilon> / 4 \<and> \<bar>cdf M2 y\<bar> < \<epsilon> / 4 \<and> y \<le> x) at_bot"
-        by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot)
-      then obtain M where "\<And>y. y \<le> M \<Longrightarrow> \<bar>cdf M1 y\<bar> < \<epsilon> / 4" "\<And>y. y \<le> M \<Longrightarrow> \<bar>cdf M2 y\<bar> < \<epsilon> / 4" "M \<le> x"
+      have "(?D \<longlongrightarrow> 0) at_bot"
+        using \<open>(cdf M1 \<longlongrightarrow> 0) at_bot\<close> \<open>(cdf M2 \<longlongrightarrow> 0) at_bot\<close> by (intro tendsto_eq_intros) auto
+      then have "eventually (\<lambda>y. ?D y < \<epsilon> / 2 \<and> y \<le> x) at_bot"
+        using \<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot abs_idempotent)
+      then obtain M where "\<And>y. y \<le> M \<Longrightarrow> ?D y < \<epsilon> / 2" "M \<le> x"
         unfolding eventually_at_bot_linorder by auto
       with open_minus_countable[OF count, of "{..< M}"] obtain a where
-        "measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \<le> x" "\<bar>cdf M1 a\<bar> < \<epsilon> / 4" "\<bar>cdf M2 a\<bar> < \<epsilon> / 4"
+        "measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \<le> x" and 1: "?D a < \<epsilon> / 2"
         by auto
 
-      from \<open>\<epsilon> > 0\<close> \<open>(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)\<close> \<open>(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)\<close>
-      have "eventually (\<lambda>y. \<bar>cdf M1 y - cdf M1 x\<bar> < \<epsilon> / 4 \<and> \<bar>cdf M2 y - cdf M2 x\<bar> < \<epsilon> / 4 \<and> x < y) (at_right x)"
-        by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less)
-      then obtain N where "N > x" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>cdf M1 y - cdf M1 x\<bar> < \<epsilon> / 4"
-        "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>cdf M2 y - cdf M2 x\<bar> < \<epsilon> / 4" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> x < y"
+      have "(?D \<longlongrightarrow> ?D x) (at_right x)"
+        using M1.cdf_is_right_cont [of x] M2.cdf_is_right_cont [of x]
+        by (intro tendsto_intros) (auto simp add: continuous_within)
+      then have "eventually (\<lambda>y. \<bar>?D y - ?D x\<bar> < \<epsilon> / 2) (at_right x)"
+        using \<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less)
+      then obtain N where "N > x" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>?D y - ?D x\<bar> < \<epsilon> / 2"
         by (auto simp add: eventually_at_right[OF less_add_one])
       with open_minus_countable[OF count, of "{x <..< N}"] obtain b where "x < b" "b < N"
-          "measure M1 {b} = 0" "measure M2 {b} = 0" "\<bar>cdf M2 x - cdf M2 b\<bar> < \<epsilon> / 4" "\<bar>cdf M1 x - cdf M1 b\<bar> < \<epsilon> / 4"
+          "measure M1 {b} = 0" "measure M2 {b} = 0" and 2: "\<bar>?D b - ?D x\<bar> < \<epsilon> / 2"
         by (auto simp: abs_minus_commute)
       from \<open>a \<le> x\<close> \<open>x < b\<close> have "a < b" "a \<le> b" by auto
 
       from \<open>char M1 = char M2\<close>
-        M1.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M1 {a} = 0\<close>  \<open>measure M1 {b} = 0\<close>]
+        M1.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M1 {a} = 0\<close> \<open>measure M1 {b} = 0\<close>]
         M2.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M2 {a} = 0\<close> \<open>measure M2 {b} = 0\<close>]
       have "complex_of_real (measure M1 {a<..b}) = complex_of_real (measure M2 {a<..b})"
         by (intro LIMSEQ_unique) auto
-      then have "measure M1 {a<..b} = measure M2 {a<..b}" by auto
-      then have *: "cdf M1 b - cdf M1 a = cdf M2 b - cdf M2 a"
-        unfolding M1.cdf_diff_eq [OF \<open>a < b\<close>] M2.cdf_diff_eq [OF \<open>a < b\<close>] .
-
-      have "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) = abs (cdf M1 x - cdf M1 b + cdf M1 a)"
+      then have "?D a = ?D b"
+        unfolding of_real_eq_iff M1.cdf_diff_eq [OF \<open>a < b\<close>, symmetric] M2.cdf_diff_eq [OF \<open>a < b\<close>, symmetric] by simp
+      then have "?D x = \<bar>(?D b - ?D x) - ?D a\<bar>"
         by simp
-      also have "\<dots> \<le> abs (cdf M1 x - cdf M1 b) + abs (cdf M1 a)"
-        by (rule abs_triangle_ineq)
-      also have "\<dots> \<le> \<epsilon> / 4 + \<epsilon> / 4"
-        by (intro add_mono less_imp_le \<open>\<bar>cdf M1 a\<bar> < \<epsilon> / 4\<close> \<open>\<bar>cdf M1 x - cdf M1 b\<bar> < \<epsilon> / 4\<close>)
-      finally have 1: "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) \<le> \<epsilon> / 2" by simp
-
-      have "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) = abs (cdf M2 x - cdf M2 b + cdf M2 a)"
-        by simp
-      also have "\<dots> \<le> abs (cdf M2 x - cdf M2 b) + abs (cdf M2 a)"
-        by (rule abs_triangle_ineq)
-      also have "\<dots> \<le> \<epsilon> / 4 + \<epsilon> / 4"
-        by (intro add_mono less_imp_le \<open>\<bar>cdf M2 x - cdf M2 b\<bar> < \<epsilon> / 4\<close> \<open>\<bar>cdf M2 a\<bar> < \<epsilon> / 4\<close>)
-      finally have 2: "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) \<le> \<epsilon> / 2" by simp
-
-      have "abs (cdf M1 x - cdf M2 x) = abs ((cdf M1 x - (cdf M1 b - cdf M1 a)) -
-          (cdf M2 x - (cdf M2 b - cdf M2 a)))" by (subst *, simp)
-      also have "\<dots> \<le> abs (cdf M1 x - (cdf M1 b - cdf M1 a)) +
-          abs (cdf M2 x - (cdf M2 b - cdf M2 a))" by (rule abs_triangle_ineq4)
-      also have "\<dots> \<le> \<epsilon> / 2 + \<epsilon> / 2" by (rule add_mono [OF 1 2])
-      finally have "abs (cdf M1 x - cdf M2 x) \<le> \<epsilon>" by simp }
+      also have "\<dots> \<le> \<bar>?D b - ?D x\<bar> + \<bar>?D a\<bar>"
+        by (rule abs_triangle_ineq4)
+      also have "\<dots> \<le> \<epsilon> / 2 + \<epsilon> / 2"
+        using 1 2 by (intro add_mono) auto
+      finally have "?D x \<le> \<epsilon>" by simp }
     then show "cdf M1 x = cdf M2 x"
       by (metis abs_le_zero_iff dense_ge eq_iff_diff_eq_0)
   qed
diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Jul 05 21:23:21 2016 +0200
@@ -1256,7 +1256,7 @@
           let val T = fastype_of1 (bound_Ts, hd args) in
             (case (Option.mapPartial (ctr_sugar_of lthy) (try (fst o dest_Type) T), T <> res_T) of
               (SOME {selss, T = Type (_, Ts), ...}, true) =>
-              (case const_of (fold (curry op @) selss []) fun_t of
+              (case const_of (flat selss) fun_t of
                 SOME sel =>
                 let
                   val args' = args |> map (typ_before explore params);
diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Tue Jul 05 21:23:21 2016 +0200
@@ -36,9 +36,9 @@
 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
   by (fact mset_append)
 
-lemma subseteq_le_multiset: "A #\<subseteq># A + B"
-unfolding le_multiset_def apply (cases B; simp)
-apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
+lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B"
+unfolding less_eq_multiset_def apply (cases B; simp)
+apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified])
 apply (simp add: less_multiset\<^sub>H\<^sub>O)
 done
 
@@ -47,7 +47,7 @@
 apply (unfold prefix_def)
 apply (erule genPrefix.induct, simp_all add: add_right_mono)
 apply (erule order_trans)
-apply (simp add: less_eq_multiset_def subseteq_le_multiset)
+apply (simp add: subseteq_le_multiset)
 done
 
 (** setsum **)
diff -r ae07cd27ebf1 -r a528d24826c5 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/HOL/UNITY/Follows.thy	Tue Jul 05 21:23:21 2016 +0200
@@ -175,19 +175,7 @@
 
 
 subsection\<open>Multiset union properties (with the multiset ordering)\<close>
-(*TODO: remove when multiset is of sort ord again*)
-instantiation multiset :: (order) ordered_ab_semigroup_add
-begin
 
-definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  "M' < M \<longleftrightarrow> M' #\<subset># M"
-
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-   "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #\<subseteq># M"
-
-instance
-  by standard (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono)
-end
 
 lemma increasing_union: 
     "[| F \<in> increasing f;  F \<in> increasing g |]  
diff -r ae07cd27ebf1 -r a528d24826c5 src/Pure/Tools/ci_profile.scala
--- a/src/Pure/Tools/ci_profile.scala	Tue Jul 05 20:51:02 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Tue Jul 05 21:23:21 2016 +0200
@@ -19,10 +19,11 @@
     println(name + "=" + Outer_Syntax.quote_string(value))
   }
 
-  private def build(options: Options): Build.Results =
+  private def build(options: Options): (Build.Results, Time) =
   {
     val progress = new Console_Progress(true)
-    progress.interrupt_handler {
+    val start_time = Time.now()
+    val results = progress.interrupt_handler {
       Build.build_selection(
         options = options,
         progress = progress,
@@ -34,6 +35,8 @@
         system_mode = true,
         selection = select_sessions _)
     }
+    val end_time = Time.now()
+    (results, end_time - start_time)
   }
 
   private def load_properties(): JProperties =
@@ -85,14 +88,16 @@
     println(s"Build for Isabelle id $isabelle_id")
     pre_hook(args)
 
-    val results = build(options)
+    val (results, elapsed_time) = build(options)
 
     print_section("TIMING")
 
     val groups = results.sessions.map(results.info).flatMap(_.groups)
     for (group <- groups)
       println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
-    println("Overall: " + compute_timing(results, None).message_resources)
+
+    val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
+    println("Overall: " + total_timing.message_resources)
 
     if (!results.ok) {
       print_section("FAILED SESSIONS")