src/HOL/Library/Product_Vector.thy
 changeset 44066 d74182c93f04 parent 37678 0040bafffdef child 44126 ce44e70d0c47
```     1.1 --- a/src/HOL/Library/Product_Vector.thy	Mon Aug 08 10:26:26 2011 -0700
1.2 +++ b/src/HOL/Library/Product_Vector.thy	Mon Aug 08 10:32:55 2011 -0700
1.3 @@ -28,13 +28,13 @@
1.4  instance proof
1.5    fix a b :: real and x y :: "'a \<times> 'b"
1.6    show "scaleR a (x + y) = scaleR a x + scaleR a y"
1.7 -    by (simp add: expand_prod_eq scaleR_right_distrib)
1.8 +    by (simp add: prod_eq_iff scaleR_right_distrib)
1.9    show "scaleR (a + b) x = scaleR a x + scaleR b x"
1.10 -    by (simp add: expand_prod_eq scaleR_left_distrib)
1.11 +    by (simp add: prod_eq_iff scaleR_left_distrib)
1.12    show "scaleR a (scaleR b x) = scaleR (a * b) x"
1.13 -    by (simp add: expand_prod_eq)
1.14 +    by (simp add: prod_eq_iff)
1.15    show "scaleR 1 x = x"
1.16 -    by (simp add: expand_prod_eq)
1.17 +    by (simp add: prod_eq_iff)
1.18  qed
1.19
1.20  end
1.21 @@ -174,7 +174,7 @@
1.22  instance proof
1.23    fix x y :: "'a \<times> 'b"
1.24    show "dist x y = 0 \<longleftrightarrow> x = y"
1.25 -    unfolding dist_prod_def expand_prod_eq by simp
1.26 +    unfolding dist_prod_def prod_eq_iff by simp
1.27  next
1.28    fix x y z :: "'a \<times> 'b"
1.29    show "dist x y \<le> dist x z + dist y z"
1.30 @@ -373,7 +373,7 @@
1.31      unfolding norm_prod_def by simp
1.32    show "norm x = 0 \<longleftrightarrow> x = 0"
1.33      unfolding norm_prod_def
1.34 -    by (simp add: expand_prod_eq)
1.35 +    by (simp add: prod_eq_iff)
1.36    show "norm (x + y) \<le> norm x + norm y"
1.37      unfolding norm_prod_def
1.38      apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
1.39 @@ -423,7 +423,7 @@
1.40      unfolding inner_prod_def