--- a/src/HOL/Analysis/Connected.thy Sun Jan 06 17:54:49 2019 +0100
+++ b/src/HOL/Analysis/Connected.thy Mon Jan 07 10:22:22 2019 +0100
@@ -1538,7 +1538,7 @@
by auto
lemma sphere_translation:
- fixes a :: "'n::euclidean_space"
+ fixes a :: "'n::real_normed_vector"
shows "sphere (a+c) r = (+) a ` sphere c r"
apply safe
apply (rule_tac x="x-a" in image_eqI)
@@ -1546,7 +1546,7 @@
done
lemma cball_translation:
- fixes a :: "'n::euclidean_space"
+ fixes a :: "'n::real_normed_vector"
shows "cball (a+c) r = (+) a ` cball c r"
apply safe
apply (rule_tac x="x-a" in image_eqI)
@@ -1554,7 +1554,7 @@
done
lemma ball_translation:
- fixes a :: "'n::euclidean_space"
+ fixes a :: "'n::real_normed_vector"
shows "ball (a+c) r = (+) a ` ball c r"
apply safe
apply (rule_tac x="x-a" in image_eqI)