--- a/src/HOL/Hahn_Banach/Vector_Space.thy Sat Mar 10 23:45:47 2012 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Sun Mar 11 13:39:16 2012 +0100
@@ -38,9 +38,8 @@
the neutral element of scalar multiplication.
*}
-locale var_V = fixes V
-
-locale vectorspace = var_V +
+locale vectorspace =
+ fixes V
assumes non_empty [iff, intro?]: "V \<noteq> {}"
and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"