# HG changeset patch
# User huffman
# Date 1235328790 28800
# Node ID 84205156ca8a602052bc7606dfacda44d5984746
# Parent  9223483cc92706def81300094b750374468dc921
simplify some proofs

diff -r 9223483cc927 -r 84205156ca8a src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Sun Feb 22 08:52:44 2009 -0800
+++ b/src/HOL/Library/Inner_Product.thy	Sun Feb 22 10:53:10 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)