| changeset 22625 | a2967023d674 |
| parent 22442 | 15d9ed9b5051 |
| child 22636 | c40465deaf20 |
--- 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