--- 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
--- 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)
--- 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
--- 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)
--- 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"
--- 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>
--- 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)
--- 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")
--- 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})"