--- a/src/HOL/Analysis/Path_Connected.thy Thu Dec 21 20:15:04 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Dec 21 21:01:47 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]