--- a/src/HOL/RealVector.thy Sun Mar 11 13:39:16 2012 +0100
+++ b/src/HOL/RealVector.thy Sun Mar 11 13:54:08 2012 +0100
@@ -954,8 +954,7 @@
subsection {* Bounded Linear and Bilinear Operators *}
-locale bounded_linear = additive +
- constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
begin