src/HOL/Real/RealVector.thy
changeset 23113 d5cdaa3b7517
parent 22973 64d300e16370
child 23120 a34f204e9c88
     1.1 --- a/src/HOL/Real/RealVector.thy	Mon May 28 03:45:41 2007 +0200
     1.2 +++ b/src/HOL/Real/RealVector.thy	Mon May 28 04:22:44 2007 +0200
     1.3 @@ -91,29 +91,25 @@
     1.4    shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)"
     1.5  by (simp add: mult_commute)
     1.6  
     1.7 -lemma additive_scaleR_right: "additive (\<lambda>x. scaleR a x::'a::real_vector)"
     1.8 -by (rule additive.intro, rule scaleR_right_distrib)
     1.9 -
    1.10 -lemma additive_scaleR_left: "additive (\<lambda>a. scaleR a x::'a::real_vector)"
    1.11 +interpretation additive_scaleR_left:
    1.12 +  additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
    1.13  by (rule additive.intro, rule scaleR_left_distrib)
    1.14  
    1.15 -lemmas scaleR_zero_left [simp] =
    1.16 -  additive.zero [OF additive_scaleR_left, standard]
    1.17 +interpretation additive_scaleR_right:
    1.18 +  additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
    1.19 +by (rule additive.intro, rule scaleR_right_distrib)
    1.20  
    1.21 -lemmas scaleR_zero_right [simp] =
    1.22 -  additive.zero [OF additive_scaleR_right, standard]
    1.23 +lemmas scaleR_zero_left [simp] = additive_scaleR_left.zero
    1.24  
    1.25 -lemmas scaleR_minus_left [simp] =
    1.26 -  additive.minus [OF additive_scaleR_left, standard]
    1.27 +lemmas scaleR_zero_right [simp] = additive_scaleR_right.zero
    1.28  
    1.29 -lemmas scaleR_minus_right [simp] =
    1.30 -  additive.minus [OF additive_scaleR_right, standard]
    1.31 +lemmas scaleR_minus_left [simp] = additive_scaleR_left.minus
    1.32 +
    1.33 +lemmas scaleR_minus_right [simp] = additive_scaleR_right.minus
    1.34  
    1.35 -lemmas scaleR_left_diff_distrib =
    1.36 -  additive.diff [OF additive_scaleR_left, standard]
    1.37 +lemmas scaleR_left_diff_distrib = additive_scaleR_left.diff
    1.38  
    1.39 -lemmas scaleR_right_diff_distrib =
    1.40 -  additive.diff [OF additive_scaleR_right, standard]
    1.41 +lemmas scaleR_right_diff_distrib = additive_scaleR_right.diff
    1.42  
    1.43  lemma scaleR_eq_0_iff [simp]:
    1.44    fixes x :: "'a::real_vector"