diff -r ed5ddf9fcc77 -r 9ba11d41cd1f src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Sep 12 09:57:33 2011 -0400
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Sep 12 09:21:01 2011 -0700
@@ -275,23 +275,6 @@
 
 subsubsection {* Type @{typ complex} *}
 
- (* TODO: move these to Complex.thy/Inner_Product.thy *)
-
-lemma norm_ii [simp]: "norm ii = 1"
-  unfolding i_def by simp
-
-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
-
 instantiation complex :: euclidean_space
 begin