# HG changeset patch
# User immler
# Date 1546852942 -3600
# Node ID d692ef26021ef69836cecd9511af43cd4acab385
# Parent  42cc3609fedfb1bf572b4c68af8fa0f11ab7bc47
generalized

diff -r 42cc3609fedf -r d692ef26021e src/HOL/Analysis/Connected.thy
--- 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)