--- a/src/HOL/Library/Product_Vector.thy Fri Jun 12 16:04:55 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy Fri Jun 12 16:23:07 2009 -0700
@@ -381,10 +381,10 @@
by (simp add: inner_commute)
show "inner (x + y) z = inner x z + inner y z"
unfolding inner_prod_def
- by (simp add: inner_left_distrib)
+ by (simp add: inner_add_left)
show "inner (scaleR r x) y = r * inner x y"
unfolding inner_prod_def
- by (simp add: inner_scaleR_left right_distrib)
+ by (simp add: right_distrib)
show "0 \<le> inner x x"
unfolding inner_prod_def
by (intro add_nonneg_nonneg inner_ge_zero)