interpretation bounded_linear_of_real
authorhuffman
Tue Apr 10 21:51:08 2007 +0200 (2007-04-10)
changeset 22625a2967023d674
parent 22624 7a6c8ed516ab
child 22626 7e35b6c8ab5b
interpretation bounded_linear_of_real
src/HOL/Real/RealVector.thy
     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