# HG changeset patch
# User nipkow
# Date 1513886507 -3600
# Node ID 2c9694a8c000c5bc9a780955d446e15307504913
# Parent  d0ca4e41883952e6c8bccbe30062f940fda45f0b
tuned op's

diff -r d0ca4e418839 -r 2c9694a8c000 src/HOL/Analysis/Path_Connected.thy
--- 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]