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

diff -r 1fe0ec14a90a -r b2d2584ace51 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Dec 21 19:09:18 2017 +0100
+++ b/src/HOL/Analysis/Connected.thy	Thu Dec 21 19:55:41 2017 +0100
@@ -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)