1.1 --- a/src/HOL/Complex.thy	Thu Aug 18 19:53:03 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Thu Aug 18 21:23:31 2011 -0700
     1.3 @@ -339,12 +339,23 @@
     1.4  
     1.5  subsection {* Completeness of the Complexes *}
     1.6  
     1.7 -interpretation Re: bounded_linear "Re"
     1.8 +lemma bounded_linear_Re: "bounded_linear Re"
     1.9    by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
    1.10  
    1.11 -interpretation Im: bounded_linear "Im"
    1.12 +lemma bounded_linear_Im: "bounded_linear Im"
    1.13    by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
    1.14  
    1.15 +lemmas tendsto_Re [tendsto_intros] =
    1.16 +  bounded_linear.tendsto [OF bounded_linear_Re]
    1.17 +
    1.18 +lemmas tendsto_Im [tendsto_intros] =
    1.19 +  bounded_linear.tendsto [OF bounded_linear_Im]
    1.20 +
    1.21 +lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
    1.22 +lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
    1.23 +lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
    1.24 +lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
    1.25 +
    1.26  lemma tendsto_Complex [tendsto_intros]:
    1.27    assumes "(f ---> a) net" and "(g ---> b) net"
    1.28    shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net"
    1.29 @@ -370,9 +381,9 @@
    1.30  proof
    1.31    fix X :: "nat \<Rightarrow> complex"
    1.32    assume X: "Cauchy X"
    1.33 -  from Re.Cauchy [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))"
    1.34 +  from Cauchy_Re [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))"
    1.35      by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
    1.36 -  from Im.Cauchy [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
    1.37 +  from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
    1.38      by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
    1.39    have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
    1.40      using LIMSEQ_Complex [OF 1 2] by simp
    1.41 @@ -511,10 +522,16 @@
    1.42  lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
    1.43  by (simp add: norm_mult power2_eq_square)
    1.44  
    1.45 -interpretation cnj: bounded_linear "cnj"
    1.46 +lemma bounded_linear_cnj: "bounded_linear cnj"
    1.47    using complex_cnj_add complex_cnj_scaleR
    1.48    by (rule bounded_linear_intro [where K=1], simp)
    1.49  
    1.50 +lemmas tendsto_cnj [tendsto_intros] =
    1.51 +  bounded_linear.tendsto [OF bounded_linear_cnj]
    1.52 +
    1.53 +lemmas isCont_cnj [simp] =
    1.54 +  bounded_linear.isCont [OF bounded_linear_cnj]
    1.55 +
    1.56  
    1.57  subsection{*The Functions @{term sgn} and @{term arg}*}
    1.58