# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1548158416 0
# Node ID dc85b5b3a532bbe2702a48c3ce81ba1befbb5426
# Parent  82a6047159194cc4e512bce2dfb4c4809b38ebd6
renamings and new material

diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Algebra/Complete_Lattice.thy
--- a/src/HOL/Algebra/Complete_Lattice.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -127,7 +127,7 @@
   have "least L b (Upper L A)"
   proof (rule least_UpperI)
     show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
-      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp)
+      by (meson L Lower_memI Upper_memD b_inf_B greatest_le subsetD)
     show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
       by (meson B_L b_inf_B greatest_Lower_below)
   qed (use bcarr L in auto)
@@ -589,7 +589,7 @@
   have "least L b (Upper L A)"
   proof (rule least_UpperI)
     show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
-      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp)
+      by (meson L Lower_memI Upper_memD b_inf_B greatest_le rev_subsetD)
     show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
       by (auto elim: greatest_Lower_below [OF b_inf_B])
   qed (use L bcarr in auto)
@@ -692,7 +692,7 @@
           show 1: "\<Squnion>\<^bsub>L\<^esub>A \<in> carrier L"
             by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
           show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
-            by (meson "*" False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_upper 1 all_not_in_conv assms(2) set_mp subset_trans)
+            by (meson "*" False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_upper 1 all_not_in_conv assms(2) subsetD subset_trans)
           show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
           proof (rule L.sup_least)
             show "A \<subseteq> carrier L" "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> b"
@@ -723,7 +723,7 @@
           show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
             by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans)
           show "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
-            by (meson * 1 False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_lower L.le_trans all_not_in_conv assms(3) set_mp subset_trans)
+            by (meson * 1 False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_lower L.le_trans all_not_in_conv assms(3) subsetD subset_trans)
         qed
       qed
     qed
@@ -814,7 +814,7 @@
         have "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
         proof (rule L'.LFP_lowerbound, simp_all)
           show "x \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
-            using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least set_rev_mp)    
+            using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least rev_subsetD)    
           with x show "f x \<sqsubseteq>\<^bsub>L\<^esub> x"
             by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI)
         qed
@@ -884,7 +884,7 @@
             moreover have "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
               by (simp add: AL L.inf_lower c)
             ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> y"
-              by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp w)
+              by (meson AL L.inf_closed L.le_trans c pf_w rev_subsetD w)
           qed
           thus ?thesis
             by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Algebra/Group_Action.thy
--- a/src/HOL/Algebra/Group_Action.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Group_Action.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -902,7 +902,7 @@
   hence "\<phi>: H \<rightarrow> carrier (BijGroup E)"
     by (simp add: BijGroup_def bij_prop0 subset_eq)
   thus "\<phi>: H \<rightarrow> carrier (BijGroup E) \<and> (\<forall>x \<in> H. \<forall>y \<in> H. \<phi> (x \<otimes> y) = \<phi> x \<otimes>\<^bsub>BijGroup E\<^esub> \<phi> y)"
-    by (simp add: S0  group_hom group_hom.hom_mult set_rev_mp)
+    by (simp add: S0  group_hom group_hom.hom_mult rev_subsetD)
 qed
 
 theorem (in group_action) induced_action:
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Ideal.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -481,7 +481,7 @@
   qed
 next
   show "I <+> J \<subseteq> Idl (I \<union> J)"
-    by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp)
+    by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def subsetD)
 qed
 
 subsection \<open>Properties of Principal Ideals\<close>
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Algebra/Polynomials.thy
--- a/src/HOL/Algebra/Polynomials.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Polynomials.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -413,7 +413,7 @@
         using A(2-3) subringE(2)[OF K] by auto
       hence "set (map2 (\<oplus>) p1 p2') \<subseteq> K"
         using A(1) subringE(7)[OF K]
-        by (induct p1) (auto, metis set_ConsD set_mp set_zip_leftD set_zip_rightD)
+        by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD)
       thus ?thesis
         unfolding p2'_def using normalize_gives_polynomial A(3) by simp
     qed }
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -665,6 +665,13 @@
    "S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
   by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)
 
+lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U \<inter> S)"
+proof -
+  have "(\<lambda>T. \<exists>Sa. T = Sa \<inter> S \<and> Sa \<subseteq> U) = (\<lambda>Sa. Sa \<subseteq> U \<and> Sa \<subseteq> S)"
+    by force
+  then show ?thesis
+    by (simp add: subtopology_def) (simp add: discrete_topology_def)
+qed
 lemma openin_Int_derived_set_of_subset:
    "openin X S \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> T)"
   by (auto simp: derived_set_of_def)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -3720,7 +3720,7 @@
           by (auto simp: algebra_simps)
         have "x \<in> T" "x \<noteq> a" using that by auto
         then have axa: "a + (x - a) \<in> affine hull S"
-           by (metis (no_types) add.commute affS diff_add_cancel set_rev_mp)
+           by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD)
         then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
           using \<open>x \<noteq> a\<close> dd1 by fastforce
         with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> a"
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -139,7 +139,7 @@
 lemma (in algebra) lambda_system_algebra:
   "positive M f \<Longrightarrow> algebra \<Omega> (lambda_system \<Omega> M f)"
   apply (auto simp add: algebra_iff_Un)
-  apply (metis lambda_system_sets set_mp sets_into_space)
+  apply (metis lambda_system_sets subsetD sets_into_space)
   apply (metis lambda_system_empty)
   apply (metis lambda_system_Compl)
   apply (metis lambda_system_Un)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -3068,7 +3068,7 @@
     then have contfb: "continuous_on (ball z d) f"
       using contf continuous_on_subset by blast
     obtain h where "\<forall>y\<in>ball z d. (h has_field_derivative f y) (at y within ball z d)"
-      by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff set_mp)
+      by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff subsetD)
     then have "\<forall>y\<in>ball z d. (h has_field_derivative f y) (at y within s)"
       by (metis open_ball at_within_open d os subsetCE)
     then have "\<exists>h. (\<forall>y. cmod (y - z) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))"
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -2849,7 +2849,7 @@
         using "2.prems"(8) that
         apply blast
         apply (metis Diff_iff Diff_insert2 contra_subsetD pg(4) that)
-        by (meson DiffD2 cp(4) set_rev_mp subset_insertI that)
+        by (meson DiffD2 cp(4) rev_subsetD subset_insertI that)
       have "winding_number g' p' = winding_number g p'
           + winding_number (pg +++ cp +++ reversepath pg) p'" unfolding g'_def
         apply (subst winding_number_join)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Derivative.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -1400,7 +1400,7 @@
     apply auto
     done
   moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
-    by (metis gf imageE interiorE set_mp that)
+    by (metis gf imageE interiorE subsetD that)
   ultimately show ?thesis using assms
     by (metis has_derivative_inverse_basic_x open_interior)
 qed
@@ -2740,7 +2740,7 @@
     using f' g' closure_subset[of T] closure_subset[of S]
     unfolding has_derivative_within_If_eq
     by (intro conjI bl tendsto_If_within_closures x_in)
-      (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
+      (auto simp: has_derivative_within inverse_eq_divide connect connect' subsetD)
 qed
 
 lemma has_vector_derivative_If_within_closures:
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -2696,7 +2696,7 @@
         by (auto simp: closure_sequential)
       from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
       have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
-        by (auto simp: set_mp extension)
+        by (auto simp: subsetD extension)
       then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
         using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
         by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -1009,7 +1009,7 @@
       fix y
       assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
       then show "\<forall>T\<in>\<G>. y \<in> T"
-        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
+        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] subsetD subg)
       show "dist y x < e"
         by (metis y dist_commute mem_ball subball subsetCE)
     qed
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -1763,7 +1763,7 @@
     by auto
   moreover
   have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
-    unfolding Z_def by (auto elim: eventually_mono intro: set_mp[OF closure_subset])
+    unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset])
   have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   proof (intro allI impI)
     fix B assume "finite B" "B \<subseteq> Z"
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -4738,7 +4738,7 @@
       fix T
       assume "connected T" and TB: "T \<subseteq> - frontier B" and "a \<in> T" and "b \<in> T"
       have "a \<notin> B"
-        by (metis A_def B_def ComplD \<open>a \<in> A\<close> assms(1) closed_open connected_component_subset in_closure_connected_component set_mp)
+        by (metis A_def B_def ComplD \<open>a \<in> A\<close> assms(1) closed_open connected_component_subset in_closure_connected_component subsetD)
       have "T \<inter> B \<noteq> {}"
         using \<open>b \<in> B\<close> \<open>b \<in> T\<close> by blast
       moreover have "T - B \<noteq> {}"
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Homotopy.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -2470,7 +2470,7 @@
     then have *: "openin ?SS (F y t) \<and> path_connected (G y t) \<and> y \<in> F y t \<and> F y t \<subseteq> G y t \<and> G y t \<subseteq> t"
       using 1 \<open>y \<in> t\<close> by presburger
     have "G y t \<subseteq> path_component_set t y"
-      using * path_component_maximal set_rev_mp by blast
+      using * path_component_maximal rev_subsetD by blast
     then have "\<exists>A. openin ?SS A \<and> y \<in> A \<and> A \<subseteq> path_component_set t x"
       by (metis "*" \<open>G y t \<subseteq> path_component_set t y\<close> dual_order.trans path_component_eq y)
   }
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -69,7 +69,7 @@
             by (simp only: u'v' max_absorb2 min_absorb1)
                (intro continuous_on_subset[OF contg'], insert u'v', auto)
         have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})"
-           using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto
+           using asm by (intro has_field_derivative_subset[OF derivg] subsetD[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto
         hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow>
                       (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
             by (simp only: u'v' max_absorb2 min_absorb1)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -2851,7 +2851,7 @@
        and cc: "connected_component (- frontier s) x y"
     have "connected_component_set (- frontier s) x \<inter> frontier s \<noteq> {}"
       apply (rule connected_Int_frontier, simp)
-      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq set_rev_mp x)
+      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq rev_subsetD x)
       using  y cc
       by blast
     then have "bounded (connected_component_set (- frontier s) x)"
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -275,7 +275,7 @@
   hence "\<Union>X = (\<Union>n. from_nat_into X n)"
     using assms by (auto cong del: SUP_cong)
   also have "\<dots> \<in> M" using assms
-    by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into set_mp)
+    by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into subsetD)
   finally show ?thesis .
 qed simp
 
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -1588,7 +1588,7 @@
       apply (rule sum.cong)
       using \<open>i \<in> D\<close> \<open>finite D\<close> sum.delta'[of D i "(\<lambda>k. inverse (2 * real (card D)))"]
         d1 assms(2)
-      by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)])
+      by (auto simp: inner_Basis rev_subsetD[OF _ assms(2)])
   }
   note ** = this
   show ?thesis
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -914,7 +914,7 @@
       have "interior m \<inter> interior (\<Union>p) = {}"
       proof (rule Int_interior_Union_intervals)
         show "\<And>T. T\<in>p \<Longrightarrow> interior m \<inter> interior T = {}"
-          by (metis DiffD1 DiffD2 that r1(1) r1(7) set_rev_mp)
+          by (metis DiffD1 DiffD2 that r1(1) r1(7) rev_subsetD)
       qed (use divp in auto)
       then show "interior S \<inter> interior m = {}"
         unfolding divp by auto
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -154,7 +154,7 @@
   proof
     assume ?lhs
     then have "0 < r'"
-      by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less set_mp)
+      by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less subsetD)
     then have "(cball a r \<subseteq> cball a' r')"
       by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
     then show ?rhs
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Auth/Message.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -243,7 +243,7 @@
 by (metis parts_idem parts_increasing parts_mono subset_trans)
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
-by (metis parts_subset_iff set_mp)
+by (metis parts_subset_iff subsetD)
 
 text\<open>Cut\<close>
 lemma parts_cut:
@@ -672,7 +672,7 @@
 lemma Fake_parts_insert_in_Un:
      "\<lbrakk>Z \<in> parts (insert X H);  X \<in> synth (analz H)\<rbrakk> 
       \<Longrightarrow> Z \<in> synth (analz H) \<union> parts H"
-by (metis Fake_parts_insert set_mp)
+by (metis Fake_parts_insert subsetD)
 
 text\<open>\<^term>\<open>H\<close> is sometimes \<^term>\<open>Key ` KK \<union> spies evs\<close>, so can't put 
   \<^term>\<open>G=H\<close>.\<close>
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -1643,7 +1643,7 @@
   unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
   have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
   have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
-  using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
+  using AsB L apply safe by (metis "0" UN_I subsetD wo_rel.isLimOrd_succ)
   assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
   have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
   proof safe
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -814,7 +814,7 @@
             with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 \<union> {z}" unfolding support_def by auto
             from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto
             have f0: "f0 \<in> F" using x0min g0(1)
-              Func_elim[OF set_mp[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
+              Func_elim[OF subsetD[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
               unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem)
             from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def
               by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
@@ -1409,7 +1409,7 @@
       from f \<open>t \<noteq> {}\<close> False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
         unfolding Field_def embed_def under_def bij_betw_def by auto
       with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
-        using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF under_Field[of r]] by blast
+        using embed_in_Field[OF r.WELL f] s.zero_under subsetD[OF under_Field[of r]] by blast
       with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
         unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
         by (fastforce intro: s.leq_zero_imp)+
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -481,7 +481,7 @@
   have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
   assume "\<forall>a\<in>A.  b \<notin> under a"
   hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
-  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp)
+  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def rev_subsetD)
   have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto
   thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
 qed
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Cardinals/Wellorder_Extension.thy
--- a/src/HOL/Cardinals/Wellorder_Extension.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -52,7 +52,7 @@
   shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
   using assms
   by (simp add: chain_subset_def extension_on_def)
-     (metis (no_types) mono_Field set_mp)
+     (metis (no_types) mono_Field subsetD)
 
 lemma downset_on_empty [simp]: "downset_on {} p"
   by (auto simp: downset_on_def)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -40,7 +40,7 @@
 assumes "inFr ns tr t" and "ns \<subseteq> ns'"
 shows "inFr ns' tr t"
 using assms apply(induct arbitrary: ns' rule: inFr.induct)
-using Base Ind by (metis inFr.simps set_mp)+
+using Base Ind by (metis inFr.simps subsetD)+
 
 lemma inFr_Ind_minus:
 assumes "inFr ns1 tr1 t" and "Inr tr1 \<in> cont tr"
@@ -111,7 +111,7 @@
 assumes "inItr ns tr n" and "ns \<subseteq> ns'"
 shows "inItr ns' tr n"
 using assms apply(induct arbitrary: ns' rule: inItr.induct)
-using Base Ind by (metis inItr.simps set_mp)+
+using Base Ind by (metis inItr.simps subsetD)+
 
 
 (* The subtree relation *)
@@ -137,7 +137,7 @@
 assumes "subtr ns tr1 tr2" and "ns \<subseteq> ns'"
 shows "subtr ns' tr1 tr2"
 using assms apply(induct arbitrary: ns' rule: subtr.induct)
-using Refl Step by (metis subtr.simps set_mp)+
+using Refl Step by (metis subtr.simps subsetD)+
 
 lemma subtr_trans_Un:
 assumes "subtr ns12 tr1 tr2" and "subtr ns23 tr2 tr3"
@@ -188,7 +188,7 @@
 assumes "subtr2 ns tr1 tr2" and "ns \<subseteq> ns'"
 shows "subtr2 ns' tr1 tr2"
 using assms apply(induct arbitrary: ns' rule: subtr2.induct)
-using Refl Step by (metis subtr2.simps set_mp)+
+using Refl Step by (metis subtr2.simps subsetD)+
 
 lemma subtr2_trans_Un:
 assumes "subtr2 ns12 tr1 tr2" and "subtr2 ns23 tr2 tr3"
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/IMP/Abs_Int2.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -38,7 +38,7 @@
 begin
 
 lemma in_gamma_inf: "x \<in> \<gamma> a1 \<Longrightarrow> x \<in> \<gamma> a2 \<Longrightarrow> x \<in> \<gamma>(a1 \<sqinter> a2)"
-by (metis IntI inter_gamma_subset_gamma_inf set_mp)
+by (metis IntI inter_gamma_subset_gamma_inf subsetD)
 
 lemma gamma_inf: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
 by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/IMP/Collecting.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -184,10 +184,10 @@
     by(fastforce simp: strip_eq_Seq step_def post_def last_append annos_ne)
 next
   case IfTrue thus ?case apply(auto simp: strip_eq_If step_def post_def)
-    by (metis (lifting,full_types) mem_Collect_eq set_mp)
+    by (metis (lifting,full_types) mem_Collect_eq subsetD)
 next
   case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
-    by (metis (lifting,full_types) mem_Collect_eq set_mp)
+    by (metis (lifting,full_types) mem_Collect_eq subsetD)
 next
   case (WhileTrue b s1 c' s2 s3)
   from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/IMP/Live.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -87,13 +87,13 @@
 next
   case (WhileFalse b s c)
   hence "~ bval b t"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
-  thus ?case by(metis WhileFalse.prems L_While_X big_step.WhileFalse set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
+  thus ?case by(metis WhileFalse.prems L_While_X big_step.WhileFalse subsetD)
 next
   case (WhileTrue b s1 c s2 s3 X t1)
   let ?w = "WHILE b DO c"
   from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems
     by (blast)
   from WhileTrue.IH(1)[OF this] obtain t2 where
@@ -151,14 +151,14 @@
   thus ?case using \<open>~bval b t\<close> by auto
 next
   case (WhileFalse b s c)
-  hence "~ bval b t" by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+  hence "~ bval b t" by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   thus ?case
-    by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse set_mp)
+    by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse subsetD)
 next
   case (WhileTrue b s1 c s2 s3 X t1)
   let ?w = "WHILE b DO c"
   from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   have "s1 = t1 on L c (L ?w X)"
     using L_While_pfp WhileTrue.prems by blast
   from WhileTrue.IH(1)[OF this] obtain t2 where
@@ -237,15 +237,15 @@
 next
   case (WhileFalse b s c)
   hence "~ bval b t"
-    by auto (metis L_While_vars bval_eq_if_eq_on_vars set_rev_mp)
+    by auto (metis L_While_vars bval_eq_if_eq_on_vars rev_subsetD)
   thus ?case using WhileFalse
-    by auto (metis L_While_X big_step.WhileFalse set_mp)
+    by auto (metis L_While_X big_step.WhileFalse subsetD)
 next
   case (WhileTrue b s1 bc' s2 s3 w X t1)
   then obtain c' where w: "w = WHILE b DO c'"
     and bc': "bc' = bury c' (L (WHILE b DO c') X)" by auto
   from \<open>bval b s1\<close> WhileTrue.prems w have "bval b t1"
-    by auto (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by auto (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   note IH = WhileTrue.hyps(3,5)
   have "s1 = t1 on L c' (L w X)"
     using L_While_pfp WhileTrue.prems w by blast
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/IMP/Live_True.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -88,13 +88,13 @@
 next
   case (WhileFalse b s c)
   hence "~ bval b t"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   thus ?case using WhileFalse.prems L_While_X[of X b c] by auto
 next
   case (WhileTrue b s1 c s2 s3 X t1)
   let ?w = "WHILE b DO c"
   from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   have "s1 = t1 on L c (L ?w X)" using  L_While_pfp WhileTrue.prems
     by (blast)
   from WhileTrue.IH(1)[OF this] obtain t2 where
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Library/Countable_Set_Type.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -150,8 +150,8 @@
 lemmas contra_csubsetD[no_atp] = contra_subsetD[Transfer.transferred]
 lemmas csubset_refl = subset_refl[Transfer.transferred]
 lemmas csubset_trans = subset_trans[Transfer.transferred]
-lemmas cset_rev_mp = set_rev_mp[Transfer.transferred]
-lemmas cset_mp = set_mp[Transfer.transferred]
+lemmas cset_rev_mp = rev_subsetD[Transfer.transferred]
+lemmas cset_mp = subsetD[Transfer.transferred]
 lemmas csubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
 lemmas eq_cmem_trans = eq_mem_trans[Transfer.transferred]
 lemmas csubset_antisym[intro!] = subset_antisym[Transfer.transferred]
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Library/Disjoint_Sets.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -58,6 +58,49 @@
     by (auto simp flip: INT_Int_distrib)
 qed
 
+lemma diff_Union_pairwise_disjoint:
+  assumes "pairwise disjnt \<A>" "\<B> \<subseteq> \<A>"
+  shows "\<Union>\<A> - \<Union>\<B> = \<Union>(\<A> - \<B>)"
+proof -
+  have "False"
+    if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B
+  proof -
+    have "A \<inter> B = {}"
+      using assms disjointD AB by blast
+  with x show ?thesis
+    by blast
+  qed
+  then show ?thesis by auto
+qed
+
+lemma Int_Union_pairwise_disjoint:
+  assumes "pairwise disjnt (\<A> \<union> \<B>)"
+  shows "\<Union>\<A> \<inter> \<Union>\<B> = \<Union>(\<A> \<inter> \<B>)"
+proof -
+  have "False"
+    if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B
+  proof -
+    have "A \<inter> B = {}"
+      using assms disjointD AB by blast
+  with x show ?thesis
+    by blast
+  qed
+  then show ?thesis by auto
+qed
+
+lemma psubset_Union_pairwise_disjoint:
+  assumes \<B>: "pairwise disjnt \<B>" and "\<A> \<subset> \<B> - {{}}"
+  shows "\<Union>\<A> \<subset> \<Union>\<B>"
+  unfolding psubset_eq
+proof
+  show "\<Union>\<A> \<subseteq> \<Union>\<B>"
+    using assms by blast
+  have "\<A> \<subseteq> \<B>" "\<Union>(\<B> - \<A> \<inter> (\<B> - {{}})) \<noteq> {}"
+    using assms by blast+
+  then show "\<Union>\<A> \<noteq> \<Union>\<B>"
+    using diff_Union_pairwise_disjoint [OF \<B>] by blast
+qed
+
 subsubsection "Family of Disjoint Sets"
 
 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Library/FSet.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -236,8 +236,8 @@
 lemmas contra_fsubsetD[no_atp] = contra_subsetD[Transfer.transferred]
 lemmas fsubset_refl = subset_refl[Transfer.transferred]
 lemmas fsubset_trans = subset_trans[Transfer.transferred]
-lemmas fset_rev_mp = set_rev_mp[Transfer.transferred]
-lemmas fset_mp = set_mp[Transfer.transferred]
+lemmas fset_rev_mp = rev_subsetD[Transfer.transferred]
+lemmas fset_mp = subsetD[Transfer.transferred]
 lemmas fsubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
 lemmas eq_fmem_trans = eq_mem_trans[Transfer.transferred]
 lemmas fsubset_antisym[intro!] = subset_antisym[Transfer.transferred]
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -154,7 +154,7 @@
 lemma
   "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
    (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
-by (metis mem_Collect_eq imageI set_rev_mp)
+by (metis mem_Collect_eq imageI rev_subsetD)
 
 lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
 by (metis (lifting) imageE)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Metis_Examples/Big_O.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -314,7 +314,7 @@
 by (metis bigo_mult bigo_refl set_times_mono3 subset_trans)
 
 lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"
-by (metis bigo_mult set_rev_mp set_times_intro)
+by (metis bigo_mult rev_subsetD set_times_intro)
 
 lemma bigo_mult4 [intro]:"f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"
 by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -78,7 +78,7 @@
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct)
-   apply (metis parts.Inj set_rev_mp)
+   apply (metis parts.Inj rev_subsetD)
   apply (metis parts.Fst)
  apply (metis parts.Snd)
 by (metis parts.Body)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Probability/Conditional_Expectation.thy
--- a/src/HOL/Probability/Conditional_Expectation.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Probability/Conditional_Expectation.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -438,7 +438,7 @@
 proof (rule nn_cond_exp_charact, auto)
   interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
   fix A assume [measurable]: "A \<in> sets F"
-  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
+  then have [measurable]: "A \<in> sets G" using assms(2) by (meson subsetD subalgebra_def)
 
   have "set_nn_integral M A (nn_cond_exp M G f) = (\<integral>\<^sup>+ x. indicator A x * nn_cond_exp M G f x\<partial>M)"
     by (metis (no_types) mult.commute)
@@ -1032,7 +1032,7 @@
   show "integrable M (real_cond_exp M G f)" by (auto simp add: assms G.real_cond_exp_int(1))
 
   fix A assume [measurable]: "A \<in> sets F"
-  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
+  then have [measurable]: "A \<in> sets G" using assms(2) by (meson subsetD subalgebra_def)
   have "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A f"
     by (rule G.real_cond_exp_intA[symmetric], auto simp add: assms(3))
   also have "... = set_lebesgue_integral M A (real_cond_exp M F f)"
@@ -1046,7 +1046,7 @@
   shows "AE x in M. real_cond_exp M F (\<lambda>x. \<Sum>i\<in>I. f i x) x = (\<Sum>i\<in>I. real_cond_exp M F (f i) x)"
 proof (rule real_cond_exp_charact)
   fix A assume [measurable]: "A \<in> sets F"
-  then have A_meas [measurable]: "A \<in> sets M" by (meson set_mp subalg subalgebra_def)
+  then have A_meas [measurable]: "A \<in> sets M" by (meson subsetD subalg subalgebra_def)
   have *: "integrable M (\<lambda>x. indicator A x * f i x)" for i
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
   have **: "integrable M (\<lambda>x. indicator A x * real_cond_exp M F (f i) x)" for i
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Probability/Fin_Map.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -1094,7 +1094,7 @@
     show "range S' \<subseteq> Collect open"
       using S
       apply (auto simp add: from_nat_into countable_basis_proj S'_def)
-      apply (metis UNIV_not_empty Union_empty from_nat_into set_mp topological_basis_open[OF basis_proj] basis_proj_def)
+      apply (metis UNIV_not_empty Union_empty from_nat_into subsetD topological_basis_open[OF basis_proj] basis_proj_def)
       done
     show "Collect open \<subseteq> Pow (space borel)" by simp
     show "sets borel = sigma_sets (space borel) (Collect open)"
@@ -1322,7 +1322,7 @@
   unfolding mapmeasure_def
 proof (subst emeasure_distr, subst measurable_cong_sets[OF s2 refl], rule fm_measurable)
   have "X \<subseteq> space (Pi\<^sub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
-  from assms inj_on_fm[of "\<lambda>_. N"] set_mp[OF this] have "fm -` fm ` X \<inter> space (Pi\<^sub>M J (\<lambda>_. N)) = X"
+  from assms inj_on_fm[of "\<lambda>_. N"] subsetD[OF this] have "fm -` fm ` X \<inter> space (Pi\<^sub>M J (\<lambda>_. N)) = X"
     by (auto simp: vimage_image_eq inj_on_def)
   thus "emeasure M X = emeasure M (fm -` fm ` X \<inter> space M)" using s1
     by simp
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Probability/Projective_Limit.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -260,7 +260,7 @@
     have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
       using J J_mono K_sets \<open>n \<ge> 1\<close>
       by (simp only: emeasure_eq_measure Z_def)
-         (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] set_mp[OF K_B]
+         (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] subsetD[OF K_B]
                intro!: arg_cong[where f=ennreal]
                simp: extensional_restrict emeasure_eq_measure prod_emb_iff sets_P space_P
                      ennreal_minus measure_nonneg)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Set.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -462,18 +462,18 @@
   by (simp add: less_eq_set_def le_fun_def)
   \<comment> \<open>Rule in Modus Ponens style.\<close>
 
-lemma rev_subsetD [intro?]: "c \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> c \<in> B"
+lemma rev_subsetD [intro?,no_atp]: "c \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> c \<in> B"
   \<comment> \<open>The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.\<close>
   by (rule subsetD)
 
-lemma subsetCE [elim]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
+lemma subsetCE [elim,no_atp]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   \<comment> \<open>Classical elimination rule.\<close>
   by (auto simp add: less_eq_set_def le_fun_def)
 
 lemma subset_eq: "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   by blast
 
-lemma contra_subsetD: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
+lemma contra_subsetD [no_atp]: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
   by blast
 
 lemma subset_refl: "A \<subseteq> A"
@@ -482,12 +482,6 @@
 lemma subset_trans: "A \<subseteq> B \<Longrightarrow> B \<subseteq> C \<Longrightarrow> A \<subseteq> C"
   by (fact order_trans)
 
-lemma set_rev_mp: "x \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> x \<in> B"
-  by (rule subsetD)
-
-lemma set_mp: "A \<subseteq> B \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B"
-  by (rule subsetD)
-
 lemma subset_not_subset_eq [code]: "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
   by (fact less_le_not_le)
 
@@ -495,7 +489,7 @@
   by simp
 
 lemmas basic_trans_rules [trans] =
-  order_trans_rules set_rev_mp set_mp eq_mem_trans
+  order_trans_rules rev_subsetD subsetD eq_mem_trans
 
 
 subsubsection \<open>Equality\<close>
@@ -1947,6 +1941,8 @@
 hide_const (open) member not_member
 
 lemmas equalityI = subset_antisym
+lemmas set_mp = subsetD
+lemmas set_rev_mp = rev_subsetD
 
 ML \<open>
 val Ball_def = @{thm Ball_def}
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -22,7 +22,7 @@
   assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
   have "Domainp A z" using \<open>A z z'\<close> by force
   have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
-    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
+    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD)
   note swt=sum_with_transfer[OF assms(1,2,2), THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD, OF transfer_rules(1,2)]
   have DsI: "Domainp A (sum_with p z r t)" if "\<And>x. x \<in> t \<Longrightarrow> Domainp A (r x)" "t \<subseteq> Collect (Domainp A)" for r t
   proof cases
@@ -59,7 +59,7 @@
   fix p p' z z' X X' and s s'::"'c \<Rightarrow> _"
   assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
   have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
-    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
+    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD)
   show "(\<exists>t u. finite t \<and> t \<subseteq> X \<and> sum_with p z (\<lambda>v. s (u v) v) t = z \<and> (\<exists>v\<in>t. u v \<noteq> 0)) =
     (\<exists>t u. finite t \<and> t \<subseteq> X' \<and> sum_with p' z' (\<lambda>v. s' (u v) v) t = z' \<and> (\<exists>v\<in>t. u v \<noteq> 0))"
     apply (transfer_prover_start, transfer_step+)
diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Vector_Spaces.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -817,7 +817,7 @@
     by (simp add: vs1.extend_basis_superset[OF i] vs1.span_mono)
   then show "x \<in> range (construct B f)"
     using f2 x by (metis (no_types) construct_basis[OF i, of _ f]
-        vs1.span_extend_basis[OF i] set_mp span_image spans_image)
+        vs1.span_extend_basis[OF i] subsetD span_image spans_image)
 qed
 
 lemma range_construct_eq_span: