src/HOL/Analysis/Inner_Product.thy
changeset 68499 d4312962161a
parent 68073 fad29d2a17a5
child 68611 4bc4b5c0ccfc
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Mon Jun 25 14:06:50 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Tue Jun 26 14:51:18 2018 +0100
     1.3 @@ -322,9 +322,9 @@
     1.4      unfolding inner_complex_def by simp
     1.5    show "inner x x = 0 \<longleftrightarrow> x = 0"
     1.6      unfolding inner_complex_def
     1.7 -    by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
     1.8 +    by (simp add: add_nonneg_eq_0_iff complex_eq_iff)
     1.9    show "norm x = sqrt (inner x x)"
    1.10 -    unfolding inner_complex_def complex_norm_def
    1.11 +    unfolding inner_complex_def norm_complex_def
    1.12      by (simp add: power2_eq_square)
    1.13  qed
    1.14