src/HOL/Real/RealVector.thy
changeset 22625 a2967023d674
parent 22442 15d9ed9b5051
child 22636 c40465deaf20
     1.1 --- a/src/HOL/Real/RealVector.thy	Tue Apr 10 21:50:08 2007 +0200
     1.2 +++ b/src/HOL/Real/RealVector.thy	Tue Apr 10 21:51:08 2007 +0200
     1.3 @@ -664,4 +664,10 @@
     1.4  apply (simp add: norm_scaleR)
     1.5  done
     1.6  
     1.7 +interpretation bounded_linear_of_real:
     1.8 +  bounded_linear ["\<lambda>r. of_real r"]
     1.9 +apply (unfold of_real_def)
    1.10 +apply (rule bounded_bilinear_scaleR.bounded_linear_left)
    1.11 +done
    1.12 +
    1.13  end