interpretation bounded_linear_of_real

--- a/src/HOL/Real/RealVector.thy	Tue Apr 10 21:50:08 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Tue Apr 10 21:51:08 2007 +0200
@@ -664,4 +664,10 @@
 apply (simp add: norm_scaleR)
 done
 
+interpretation bounded_linear_of_real:
+  bounded_linear ["\<lambda>r. of_real r"]
+apply (unfold of_real_def)
+apply (rule bounded_bilinear_scaleR.bounded_linear_left)
+done
+
 end