# HG changeset patch
# User nipkow
# Date 1513879758 -3600
# Node ID 1fe0ec14a90ac2b186c3738eb88e860d667cf7f4
# Parent  d2be0579a2c8723340728d0662b5aecc3042fdca
tuned op's

diff -r d2be0579a2c8 -r 1fe0ec14a90a src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- 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)
diff -r d2be0579a2c8 -r 1fe0ec14a90a src/HOL/Analysis/Connected.thy
--- 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
 
diff -r d2be0579a2c8 -r 1fe0ec14a90a src/HOL/Analysis/Path_Connected.thy
--- 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"