src/HOL/Library/Inner_Product.thy
changeset 49962 a8cc904a6820
parent 44902 9ba11d41cd1f
child 51002 496013a6eb38
--- a/src/HOL/Library/Inner_Product.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -201,7 +201,7 @@
   show "inner x y = inner y x"
     unfolding inner_real_def by (rule mult_commute)
   show "inner (x + y) z = inner x z + inner y z"
-    unfolding inner_real_def by (rule left_distrib)
+    unfolding inner_real_def by (rule distrib_right)
   show "inner (scaleR r x) y = r * inner x y"
     unfolding inner_real_def real_scaleR_def by (rule mult_assoc)
   show "0 \<le> inner x x"
@@ -225,9 +225,9 @@
   show "inner x y = inner y x"
     unfolding inner_complex_def by (simp add: mult_commute)
   show "inner (x + y) z = inner x z + inner y z"
-    unfolding inner_complex_def by (simp add: left_distrib)
+    unfolding inner_complex_def by (simp add: distrib_right)
   show "inner (scaleR r x) y = r * inner x y"
-    unfolding inner_complex_def by (simp add: right_distrib)
+    unfolding inner_complex_def by (simp add: distrib_left)
   show "0 \<le> inner x x"
     unfolding inner_complex_def by simp
   show "inner x x = 0 \<longleftrightarrow> x = 0"