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