--- a/src/HOL/Library/Inner_Product.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Library/Inner_Product.thy Tue Aug 02 21:30:30 2016 +0200
@@ -293,10 +293,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 ii x = Im x"
+lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
unfolding inner_complex_def by simp
-lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
+lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
unfolding inner_complex_def by simp