# HG changeset patch
# User immler
# Date 1456760115 -3600
# Node ID 87ca8b5145b870c33d3179909bee11ccfbb0109d
# Parent  2e4c6ef809b5248e51f7c0983d7729284198849b
generalized

diff -r 2e4c6ef809b5 -r 87ca8b5145b8 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 29 15:14:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 29 16:35:15 2016 +0100
@@ -3437,7 +3437,7 @@
 qed
 
 lemma bounded_uminus [simp]:
-  fixes X :: "'a::euclidean_space set"
+  fixes X :: "'a::real_normed_vector set"
   shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
 by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)