--- a/src/HOL/Library/Euclidean_Space.thy Sun Feb 22 18:16:32 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy Sun Feb 22 12:03:20 2009 -0800
@@ -1010,11 +1010,6 @@
lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm
-instantiation "^" :: (monoid_add,type) monoid_add
-begin
- instance by (intro_classes)
-end
-
lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"
apply vector
apply auto
--- a/src/HOL/Library/Inner_Product.thy Sun Feb 22 18:16:32 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy Sun Feb 22 12:03:20 2009 -0800
@@ -21,19 +21,10 @@
begin
lemma inner_zero_left [simp]: "inner 0 x = 0"
-proof -
- have "inner 0 x = inner (0 + 0) x" by simp
- also have "\<dots> = inner 0 x + inner 0 x" by (rule inner_left_distrib)
- finally show "inner 0 x = 0" by simp
-qed
+ using inner_left_distrib [of 0 0 x] by simp
lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
-proof -
- have "inner (- x) y + inner x y = inner (- x + x) y"
- by (rule inner_left_distrib [symmetric])
- also have "\<dots> = - inner x y + inner x y" by simp
- finally show "inner (- x) y = - inner x y" by simp
-qed
+ using inner_left_distrib [of x "- x" y] by simp
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
by (simp add: diff_minus inner_left_distrib)