src/HOL/Complex.thy
changeset 30729 461ee3e49ad3
parent 30273 ecd6f0ca62ea
child 30960 fec1a04b7220
     1.1 --- a/src/HOL/Complex.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/src/HOL/Complex.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -348,13 +348,13 @@
     1.4  
     1.5  subsection {* Completeness of the Complexes *}
     1.6  
     1.7 -interpretation Re!: bounded_linear "Re"
     1.8 +interpretation Re: bounded_linear "Re"
     1.9  apply (unfold_locales, simp, simp)
    1.10  apply (rule_tac x=1 in exI)
    1.11  apply (simp add: complex_norm_def)
    1.12  done
    1.13  
    1.14 -interpretation Im!: bounded_linear "Im"
    1.15 +interpretation Im: bounded_linear "Im"
    1.16  apply (unfold_locales, simp, simp)
    1.17  apply (rule_tac x=1 in exI)
    1.18  apply (simp add: complex_norm_def)
    1.19 @@ -516,7 +516,7 @@
    1.20  lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
    1.21  by (simp add: norm_mult power2_eq_square)
    1.22  
    1.23 -interpretation cnj!: bounded_linear "cnj"
    1.24 +interpretation cnj: bounded_linear "cnj"
    1.25  apply (unfold_locales)
    1.26  apply (rule complex_cnj_add)
    1.27  apply (rule complex_cnj_scaleR)