src/HOL/Library/Product_Vector.thy
changeset 44282 f0de18b62d63
parent 44233 aa74ce315bae
child 44568 e6f291cb5810
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -489,11 +489,11 @@
     1.4  
     1.5  subsection {* Pair operations are linear *}
     1.6  
     1.7 -interpretation fst: bounded_linear fst
     1.8 +lemma bounded_linear_fst: "bounded_linear fst"
     1.9    using fst_add fst_scaleR
    1.10    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    1.11  
    1.12 -interpretation snd: bounded_linear snd
    1.13 +lemma bounded_linear_snd: "bounded_linear snd"
    1.14    using snd_add snd_scaleR
    1.15    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    1.16