--- 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)
--- 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
--- 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':
--- 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"
--- 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