--- 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