--- 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)