--- a/src/HOL/Analysis/Inner_Product.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Tue Feb 28 13:51:47 2017 +0000
@@ -298,10 +298,10 @@
lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
unfolding inner_complex_def by simp
-lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
+lemma complex_inner_i_left [simp]: "inner \<i> x = Im x"
unfolding inner_complex_def by simp
-lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
+lemma complex_inner_i_right [simp]: "inner x \<i> = Im x"
unfolding inner_complex_def by simp