--- a/src/HOL/Real/RealVector.thy Tue May 29 17:37:04 2007 +0200
+++ b/src/HOL/Real/RealVector.thy Tue May 29 18:19:56 2007 +0200
@@ -756,6 +756,11 @@
bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
by (rule bounded_bilinear_mult.bounded_linear_right)
+interpretation bounded_linear_divide:
+ bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
+unfolding divide_inverse
+by (rule bounded_bilinear_mult.bounded_linear_left)
+
interpretation bounded_bilinear_scaleR:
bounded_bilinear ["scaleR"]
apply (rule bounded_bilinear.intro)