1.1 --- a/src/HOL/Complex.thy	Tue Aug 09 10:42:07 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Tue Aug 09 12:50:22 2011 -0700
     1.3 @@ -340,16 +340,10 @@
     1.4  subsection {* Completeness of the Complexes *}
     1.5  
     1.6  interpretation Re: bounded_linear "Re"
     1.7 -apply (unfold_locales, simp, simp)
     1.8 -apply (rule_tac x=1 in exI)
     1.9 -apply (simp add: complex_norm_def)
    1.10 -done
    1.11 +  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
    1.12  
    1.13  interpretation Im: bounded_linear "Im"
    1.14 -apply (unfold_locales, simp, simp)
    1.15 -apply (rule_tac x=1 in exI)
    1.16 -apply (simp add: complex_norm_def)
    1.17 -done
    1.18 +  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
    1.19  
    1.20  lemma tendsto_Complex [tendsto_intros]:
    1.21    assumes "(f ---> a) net" and "(g ---> b) net"
    1.22 @@ -518,11 +512,8 @@
    1.23  by (simp add: norm_mult power2_eq_square)
    1.24  
    1.25  interpretation cnj: bounded_linear "cnj"
    1.26 -apply (unfold_locales)
    1.27 -apply (rule complex_cnj_add)
    1.28 -apply (rule complex_cnj_scaleR)
    1.29 -apply (rule_tac x=1 in exI, simp)
    1.30 -done
    1.31 +  using complex_cnj_add complex_cnj_scaleR
    1.32 +  by (rule bounded_linear_intro [where K=1], simp)
    1.33  
    1.34  
    1.35  subsection{*The Functions @{term sgn} and @{term arg}*}