src/HOL/Library/ListVector.thy
changeset 49962 a8cc904a6820
parent 49961 d3d2b78b1c19
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/ListVector.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Library/ListVector.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  apply simp
     1.5  apply(case_tac zs)
     1.6  apply (simp)
     1.7 -apply(simp add: left_distrib)
     1.8 +apply(simp add: distrib_right)
     1.9  done
    1.10  
    1.11  lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
    1.12 @@ -146,7 +146,7 @@
    1.13  apply simp
    1.14  apply(case_tac ys)
    1.15  apply (simp)
    1.16 -apply (simp add: right_distrib mult_assoc)
    1.17 +apply (simp add: distrib_left mult_assoc)
    1.18  done
    1.19  
    1.20  end