src/HOL/Library/Product_Vector.thy
changeset 44127 7b57b9295d98
parent 44126 ce44e70d0c47
child 44214 1e0414bda9af
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:42:07 2011 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 09 12:50:22 2011 -0700
     1.3 @@ -435,18 +435,12 @@
     1.4  subsection {* Pair operations are linear *}
     1.5  
     1.6  interpretation fst: bounded_linear fst
     1.7 -  apply (unfold_locales)
     1.8 -  apply (rule fst_add)
     1.9 -  apply (rule fst_scaleR)
    1.10 -  apply (rule_tac x="1" in exI, simp add: norm_Pair)
    1.11 -  done
    1.12 +  using fst_add fst_scaleR
    1.13 +  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    1.14  
    1.15  interpretation snd: bounded_linear snd
    1.16 -  apply (unfold_locales)
    1.17 -  apply (rule snd_add)
    1.18 -  apply (rule snd_scaleR)
    1.19 -  apply (rule_tac x="1" in exI, simp add: norm_Pair)
    1.20 -  done
    1.21 +  using snd_add snd_scaleR
    1.22 +  by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    1.23  
    1.24  text {* TODO: move to NthRoot *}
    1.25  lemma sqrt_add_le_add_sqrt: