--- a/src/HOL/Complex.thy Tue Aug 09 10:42:07 2011 -0700
+++ b/src/HOL/Complex.thy Tue Aug 09 12:50:22 2011 -0700
@@ -340,16 +340,10 @@
subsection {* Completeness of the Complexes *}
interpretation Re: bounded_linear "Re"
-apply (unfold_locales, simp, simp)
-apply (rule_tac x=1 in exI)
-apply (simp add: complex_norm_def)
-done
+ by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
interpretation Im: bounded_linear "Im"
-apply (unfold_locales, simp, simp)
-apply (rule_tac x=1 in exI)
-apply (simp add: complex_norm_def)
-done
+ by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
lemma tendsto_Complex [tendsto_intros]:
assumes "(f ---> a) net" and "(g ---> b) net"
@@ -518,11 +512,8 @@
by (simp add: norm_mult power2_eq_square)
interpretation cnj: bounded_linear "cnj"
-apply (unfold_locales)
-apply (rule complex_cnj_add)
-apply (rule complex_cnj_scaleR)
-apply (rule_tac x=1 in exI, simp)
-done
+ using complex_cnj_add complex_cnj_scaleR
+ by (rule bounded_linear_intro [where K=1], simp)
subsection{*The Functions @{term sgn} and @{term arg}*}