# HG changeset patch
# User nipkow
# Date 1541948939 -3600
# Node ID e4d5a07fecb646a2ca0067c1032a1ec82a7ef0c1
# Parent  b9dd40e2c47084bded0b2cdd35c2a694da1536cc
tuned

diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -1190,13 +1190,13 @@
     assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U"
       and U': "U' \<subseteq> topspace X'"
     show "closedin X {x \<in> topspace X. f x \<in> U'} = closedin X' U'"
-      using U'  by (auto simp add: closedin_def Diff_subset simp flip: * [of "topspace X' - U'"] eq [OF that])
+      using U'  by (auto simp add: closedin_def simp flip: * [of "topspace X' - U'"] eq [OF that])
   next
     fix U' :: "'b set"
     assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U"
       and U': "U' \<subseteq> topspace X'"
     show "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
-      using U'  by (auto simp add: openin_closedin_eq Diff_subset simp flip: * [of "topspace X' - U'"] eq [OF that])
+      using U'  by (auto simp add: openin_closedin_eq simp flip: * [of "topspace X' - U'"] eq [OF that])
   qed
   then show ?thesis
     unfolding quotient_map_def by force
@@ -1491,7 +1491,7 @@
 
 lemma separatedin_closedin_diff:
      "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
-  apply (simp add: separatedin_def Diff_Int_distrib2 Diff_subset closure_of_minimal inf_absorb2)
+  apply (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2)
   apply (meson Diff_subset closedin_subset subset_trans)
   done
 
diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -1728,7 +1728,7 @@
   have "f ` (A - {a}) = g ` (A - {a})"
     by (intro image_cong) (simp_all add: eq)
   then have "B - {f a} = B - {g a}"
-    using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff Diff_subset)
+    using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff)
   moreover have "f a \<in> B" "g a \<in> B"
     using f g a by (auto simp: bij_betw_def)
   ultimately show ?thesis
@@ -1884,9 +1884,9 @@
     moreover obtain a where "rl a = Suc n" "a \<in> s"
       by (metis atMost_iff image_iff le_Suc_eq rl)
     ultimately have n: "{..n} = rl ` (s - {a})"
-      by (auto simp: inj_on_image_set_diff Diff_subset rl)
+      by (auto simp: inj_on_image_set_diff rl)
     have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
-      using inj_rl \<open>a \<in> s\<close> by (auto simp: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
+      using inj_rl \<open>a \<in> s\<close> by (auto simp: n inj_on_image_eq_iff[OF inj_rl])
     then show "card ?S = 1"
       unfolding card_S by simp }
 
@@ -1907,7 +1907,7 @@
 
       { fix x assume "x \<in> s" "x \<notin> {a, b}"
         then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
-          by (auto simp: eq Diff_subset inj_on_image_set_diff[OF inj])
+          by (auto simp: eq inj_on_image_set_diff[OF inj])
         also have "\<dots> = rl ` (s - {x})"
           using ab \<open>x \<notin> {a, b}\<close> by auto
         also assume "\<dots> = rl ` s"
@@ -2448,7 +2448,7 @@
       by auto
     finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
       unfolding s_eq \<open>a = enum i\<close> \<open>i = 0\<close>
-      by (simp add: Diff_subset inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
+      by (simp add: inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
 
     have "enum 0 < f' 0"
       using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono f'_eq_enum)
diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -761,7 +761,7 @@
   show ?rhs
     apply (rule_tac x="s \<inter> t" in exI)
     using st
-    apply (auto simp: Diff_subset holomorphic_on_subset)
+    apply (auto simp: holomorphic_on_subset)
     done
 next
   assume ?rhs
diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -36,7 +36,7 @@
     have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x
     proof -
       have "closedin (subtopology euclidean S) (S - V)"
-        by (simp add: Diff_Diff_Int Diff_subset closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
+        by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
       with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
         show ?thesis
           by (simp add: order_class.order.order_iff_strict)
diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -1246,7 +1246,7 @@
       case 1
       show ?thesis
         by (rule negligible_subset [of "closure S"])
-           (simp_all add: Diff_subset frontier_def negligible_lowdim 1)
+           (simp_all add: frontier_def negligible_lowdim 1)
     next
       case 2
       obtain a where a: "a \<in> interior S"
diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -1528,7 +1528,7 @@
 
   show "a \<in> {A \<in> sets M. emeasure M A \<noteq> top} \<Longrightarrow> b \<in> {A \<in> sets M. emeasure M A \<noteq> top} \<Longrightarrow>
     a - b \<in> {A \<in> sets M. emeasure M A \<noteq> top}" for a b
-    using emeasure_mono[of "a - b" a M] by (auto simp: Diff_subset top_unique)
+    using emeasure_mono[of "a - b" a M] by (auto simp: top_unique)
 qed (auto dest: sets.sets_into_space)
 
 lemma measure_nonneg[simp]: "0 \<le> measure M A"
@@ -1746,7 +1746,7 @@
   finally show  "a \<union> b \<in> fmeasurable M"
     using * by (auto intro: fmeasurableI)
   show "a - b \<in> fmeasurable M"
-    using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def Diff_subset)
+    using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def)
 qed
 
 subsection\<open>Measurable sets formed by unions and intersections\<close>
diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -5726,7 +5726,7 @@
   shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
 apply (simp add: special_hyperplane_span)
 apply (rule dim_unique [OF subset_refl])
-apply (auto simp: Diff_subset independent_substdbasis)
+apply (auto simp: independent_substdbasis)
 apply (metis member_remove remove_def span_base)
 done
 
@@ -6823,7 +6823,7 @@
     using assms orthogonal_spanningset_subspace by blast
   then show ?thesis
     apply (rule_tac B = "B - {0}" in that)
-    apply (auto simp: indep_card_eq_dim_span pairwise_subset Diff_subset pairwise_orthogonal_independent elim: pairwise_subset)
+    apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset)
     done
 qed
 
@@ -7178,7 +7178,7 @@
       have "closed S"
         by (simp add: \<open>subspace S\<close> closed_subspace)
       then show "closure (S - U) \<subseteq> S"
-        by (simp add: Diff_subset closure_minimal)
+        by (simp add: closure_minimal)
       show "S \<subseteq> closure (S - U)"
       proof (clarsimp simp: closure_approachable)
         fix x and e::real
@@ -7258,7 +7258,7 @@
     shows "closure(S - T) = closure S"
 proof
   show "closure (S - T) \<subseteq> closure S"
-    by (simp add: Diff_subset closure_mono)
+    by (simp add: closure_mono)
   have "closure (rel_interior S - T) = closure (rel_interior S)"
     apply (rule dense_complement_openin_affine_hull)
     apply (simp add: assms rel_interior_aff_dim)
diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -794,7 +794,7 @@
   by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym)
 
 lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
-  by (simp add: Diff_subset closedin_def)
+  by (simp add: closedin_def)
 
 lemma discrete_topology_unique:
    "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> (\<forall>x \<in> U. openin X {x})" (is "?lhs = ?rhs")
diff -r b9dd40e2c470 -r e4d5a07fecb6 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Nov 11 14:34:02 2018 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Nov 11 16:08:59 2018 +0100
@@ -291,7 +291,7 @@
   from B_A \<open>x \<notin> B\<close> have "B = f ` A - {x}"
     by blast
   with B_A \<open>x \<notin> B\<close> \<open>x = f y\<close> \<open>inj_on f A\<close> \<open>y \<in> A\<close> have "B = f ` (A - {y})"
-    by (simp add: inj_on_image_set_diff Set.Diff_subset)
+    by (simp add: inj_on_image_set_diff)
   moreover from \<open>inj_on f A\<close> have "inj_on f (A - {y})"
     by (rule inj_on_diff)
   ultimately have "finite (A - {y})"