src/HOL/Library/ListVector.thy
changeset 57512 cc97b347b301
parent 49962 a8cc904a6820
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/ListVector.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Library/ListVector.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  apply(simp)
     1.5  apply(case_tac zs)
     1.6   apply(simp)
     1.7 -apply(simp add: add_assoc)
     1.8 +apply(simp add: add.assoc)
     1.9  done
    1.10  
    1.11  subsection "Inner product"
    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: distrib_left mult_assoc)
    1.17 +apply (simp add: distrib_left mult.assoc)
    1.18  done
    1.19  
    1.20  end