1.1 --- a/src/HOL/Complex.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Complex.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5  definition complex_inverse_def:
     1.6    "inverse x =
     1.7 -    Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
     1.8 +    Complex (Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)) (- Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2))"
     1.9  
    1.10  definition complex_divide_def:
    1.11    "x / (y\<Colon>complex) = x * inverse y"
    1.12 @@ -128,15 +128,15 @@
    1.13    by (simp add: complex_mult_def)
    1.14  
    1.15  lemma complex_inverse [simp]:
    1.16 -  "inverse (Complex a b) = Complex (a / (a\<twosuperior> + b\<twosuperior>)) (- b / (a\<twosuperior> + b\<twosuperior>))"
    1.17 +  "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))"
    1.18    by (simp add: complex_inverse_def)
    1.19  
    1.20  lemma complex_Re_inverse:
    1.21 -  "Re (inverse x) = Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)"
    1.22 +  "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
    1.23    by (simp add: complex_inverse_def)
    1.24  
    1.25  lemma complex_Im_inverse:
    1.26 -  "Im (inverse x) = - Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)"
    1.27 +  "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
    1.28    by (simp add: complex_inverse_def)
    1.29  
    1.30  instance
    1.31 @@ -267,7 +267,7 @@
    1.32  begin
    1.33  
    1.34  definition complex_norm_def:
    1.35 -  "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
    1.36 +  "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
    1.37  
    1.38  abbreviation cmod :: "complex \<Rightarrow> real"
    1.39    where "cmod \<equiv> norm"
    1.40 @@ -283,7 +283,7 @@
    1.41  
    1.42  lemmas cmod_def = complex_norm_def
    1.43  
    1.44 -lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.45 +lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"
    1.46    by (simp add: complex_norm_def)
    1.47  
    1.48  instance proof
    1.49 @@ -439,7 +439,7 @@
    1.50  lemma i_squared [simp]: "ii * ii = -1"
    1.51    by (simp add: i_def)
    1.52  
    1.53 -lemma power2_i [simp]: "ii\<twosuperior> = -1"
    1.54 +lemma power2_i [simp]: "ii\<^sup>2 = -1"
    1.55    by (simp add: power2_eq_square)
    1.56  
    1.57  lemma inverse_i [simp]: "inverse ii = - ii"
    1.58 @@ -529,10 +529,10 @@
    1.59  lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"
    1.60    by (simp add: complex_eq_iff)
    1.61  
    1.62 -lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
    1.63 +lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
    1.64    by (simp add: complex_eq_iff power2_eq_square)
    1.65  
    1.66 -lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
    1.67 +lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<^sup>2"
    1.68    by (simp add: norm_mult power2_eq_square)
    1.69  
    1.70  lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"