# HG changeset patch
# User nipkow
# Date 1513890761 -3600
# Node ID a6d8458b48c0b713078d5e57c6f8edf579590c0d
# Parent  759d4fb30bfcdf71c46c8da16772bd0c63631131# Parent  73635a5bfa5c6e2f5e51f2248f6b70dfea54a5ed
merged

diff -r 759d4fb30bfc -r a6d8458b48c0 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Dec 21 12:19:24 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Dec 21 22:12:41 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 759d4fb30bfc -r a6d8458b48c0 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Dec 21 12:19:24 2017 +0100
+++ b/src/HOL/Analysis/Connected.thy	Thu Dec 21 22:12:41 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
@@ -3058,7 +3058,7 @@
 
 lemma sphere_translation:
   fixes a :: "'n::euclidean_space"
-  shows "sphere (a+c) r = op+a ` sphere c r"
+  shows "sphere (a+c) r = op+ a ` sphere c r"
 apply safe
 apply (rule_tac x="x-a" in image_eqI)
 apply (auto simp: dist_norm algebra_simps)
@@ -3066,7 +3066,7 @@
 
 lemma cball_translation:
   fixes a :: "'n::euclidean_space"
-  shows "cball (a+c) r = op+a ` cball c r"
+  shows "cball (a+c) r = op+ a ` cball c r"
 apply safe
 apply (rule_tac x="x-a" in image_eqI)
 apply (auto simp: dist_norm algebra_simps)
@@ -3074,7 +3074,7 @@
 
 lemma ball_translation:
   fixes a :: "'n::euclidean_space"
-  shows "ball (a+c) r = op+a ` ball c r"
+  shows "ball (a+c) r = op+ a ` ball c r"
 apply safe
 apply (rule_tac x="x-a" in image_eqI)
 apply (auto simp: dist_norm algebra_simps)
@@ -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 759d4fb30bfc -r a6d8458b48c0 src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Thu Dec 21 12:19:24 2017 +0100
+++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Dec 21 22:12:41 2017 +0100
@@ -189,7 +189,7 @@
   by(rule embed_measure_count_space')(erule subset_inj_on, simp)
 
 lemma sets_embed_measure_alt:
-    "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
+    "inj f \<Longrightarrow> sets (embed_measure M f) = (op` f) ` sets M"
   by (auto simp: sets_embed_measure)
 
 lemma emeasure_embed_measure_image':
diff -r 759d4fb30bfc -r a6d8458b48c0 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Dec 21 12:19:24 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Dec 21 22:12:41 2017 +0100
@@ -1738,7 +1738,7 @@
     case True then show ?thesis
       by (simp add: path_component_refl_eq pathstart_def)
   next
-    case False have "continuous_on {0..1} (p o (op*y))"
+    case False have "continuous_on {0..1} (p o (op* y))"
       apply (rule continuous_intros)+
       using p [unfolded path_def] y
       apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
@@ -2012,7 +2012,7 @@
     by (intro path_connected_continuous_image path_connected_punctured_universe assms)
   with eq have "path_connected (sphere (0::'a) r)"
     by auto
-  then have "path_connected(op +a ` (sphere (0::'a) r))"
+  then have "path_connected(op + a ` (sphere (0::'a) r))"
     by (simp add: path_connected_translation)
   then show ?thesis
     by (metis add.right_neutral sphere_translation)
@@ -2241,7 +2241,7 @@
   assumes "DIM('a) = 1" and "r > 0"
   obtains x y where "sphere a r = {x,y} \<and> dist x y = 2*r"
 proof -
-  have "sphere a r = op +a ` sphere 0 r"
+  have "sphere a r = op + a ` sphere 0 r"
     by (metis add.right_neutral sphere_translation)
   then show ?thesis
     using sphere_1D_doubleton_zero [OF assms]
@@ -2282,7 +2282,7 @@
   assumes 2: "2 \<le> DIM('N)" and pc: "path_connected {r. 0 \<le> r \<and> P r}"
   shows "path_connected {x. P(norm(x - a))}"
 proof -
-  have "{x. P(norm(x - a))} = op+a ` {x. P(norm x)}"
+  have "{x. P(norm(x - a))} = op+ a ` {x. P(norm x)}"
     by force
   moreover have "path_connected {x::'N. P(norm x)}"
   proof -
@@ -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"
diff -r 759d4fb30bfc -r a6d8458b48c0 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Thu Dec 21 12:19:24 2017 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Thu Dec 21 22:12:41 2017 +0100
@@ -299,7 +299,7 @@
     (auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject)
 end
 
-lemma (in preorder) tranclp_less: "op <\<^sup>+\<^sup>+ = op <"
+lemma (in preorder) tranclp_less: "op < \<^sup>+\<^sup>+ = op <"
 by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
 
 instance bit0 and bit1 :: (finite) wellorder