src/HOL/Real/HahnBanach/Subspace.thy

--- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -17,6 +17,7 @@
 *}
 
 locale subspace = var U + var V +
+  constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
   assumes non_empty [iff, intro]: "U \<noteq> {}"
     and subset [iff]: "U \<subseteq> V"
     and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"