--- a/src/HOL/Library/Inner_Product.thy Mon Sep 12 09:57:33 2011 -0400
+++ b/src/HOL/Library/Inner_Product.thy Mon Sep 12 09:21:01 2011 -0700
@@ -240,6 +240,18 @@
end
+lemma complex_inner_1 [simp]: "inner 1 x = Re x"
+ unfolding inner_complex_def by simp
+
+lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
+ unfolding inner_complex_def by simp
+
+lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
+ unfolding inner_complex_def by simp
+
+lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
+ unfolding inner_complex_def by simp
+
subsection {* Gradient derivative *}