# HG changeset patch
# User huffman
# Date 1176234668 -7200
# Node ID a2967023d674d8aedf744013b016122f64115bd3
# Parent  7a6c8ed516ab14745fb680ac2c684d64cd2c6158
interpretation bounded_linear_of_real

diff -r 7a6c8ed516ab -r a2967023d674 src/HOL/Real/RealVector.thy
--- 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