--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Dec 21 18:11:24 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Dec 21 19:09:18 2017 +0100
@@ -4149,11 +4149,11 @@
assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
shows "open {z. z \<notin> path_image \<gamma> \<and> winding_number \<gamma> z = k}"
proof -
- have op: "open (- path_image \<gamma>)"
+ have opn: "open (- path_image \<gamma>)"
by (simp add: closed_path_image \<gamma> open_Compl)
{ fix z assume z: "z \<notin> path_image \<gamma>" and k: "k = winding_number \<gamma> z"
obtain e where e: "e>0" "ball z e \<subseteq> - path_image \<gamma>"
- using open_contains_ball [of "- path_image \<gamma>"] op z
+ using open_contains_ball [of "- path_image \<gamma>"] opn z
by blast
have "\<exists>e>0. \<forall>y. dist y z < e \<longrightarrow> y \<notin> path_image \<gamma> \<and> winding_number \<gamma> y = winding_number \<gamma> z"
apply (rule_tac x=e in exI)
--- a/src/HOL/Analysis/Connected.thy Thu Dec 21 18:11:24 2017 +0100
+++ b/src/HOL/Analysis/Connected.thy Thu Dec 21 19:09:18 2017 +0100
@@ -2266,7 +2266,7 @@
J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\<close>
lemma Heine_Borel_lemma:
- assumes "compact S" and Ssub: "S \<subseteq> \<Union>\<G>" and op: "\<And>G. G \<in> \<G> \<Longrightarrow> open G"
+ assumes "compact S" and Ssub: "S \<subseteq> \<Union>\<G>" and opn: "\<And>G. G \<in> \<G> \<Longrightarrow> open G"
obtains e where "0 < e" "\<And>x. x \<in> S \<Longrightarrow> \<exists>G \<in> \<G>. ball x e \<subseteq> G"
proof -
have False if neg: "\<And>e. 0 < e \<Longrightarrow> \<exists>x \<in> S. \<forall>G \<in> \<G>. \<not> ball x e \<subseteq> G"
@@ -2280,7 +2280,7 @@
then obtain G where "l \<in> G" "G \<in> \<G>"
using Ssub by auto
then obtain e where "0 < e" and e: "\<And>z. dist z l < e \<Longrightarrow> z \<in> G"
- using op open_dist by blast
+ using opn open_dist by blast
obtain N1 where N1: "\<And>n. n \<ge> N1 \<Longrightarrow> dist (f (r n)) l < e/2"
using to_l apply (simp add: lim_sequentially)
using \<open>0 < e\<close> half_gt_zero that by blast
@@ -4566,7 +4566,7 @@
proof -
obtain \<B> :: "'a set set"
where "countable \<B>"
- and op: "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
+ and opn: "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
and Un: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
using univ_second_countable by blast
have *: "infinite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
@@ -4593,7 +4593,7 @@
done
show ?thesis
apply (rule that [OF \<open>inj f\<close> _ *])
- apply (auto simp: \<open>\<B> = range f\<close> op)
+ apply (auto simp: \<open>\<B> = range f\<close> opn)
done
qed
--- a/src/HOL/Analysis/Path_Connected.thy Thu Dec 21 18:11:24 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Dec 21 19:09:18 2017 +0100
@@ -8262,10 +8262,10 @@
by (meson Topological_Spaces.connected_continuous_image \<open>connected S\<close> homeomorphism_cont1 homeomorphism_of_subsets homhj hull_subset top_greatest)
have hUS: "h ` U \<subseteq> h ` S"
by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq)
- have op: "openin (subtopology euclidean (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
+ have opn: "openin (subtopology euclidean (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
using homeomorphism_imp_open_map [OF homhj] by simp
have "open (h ` U)" "open (h ` S)"
- by (auto intro: opeS opeU openin_trans op)
+ by (auto intro: opeS opeU openin_trans opn)
then obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g"
and f: "\<And>x. x \<in> h ` K \<Longrightarrow> f x \<in> h ` U"
and sub: "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> h ` S"