src/HOL/Power.thy
changeset 53076 47c9aff07725
parent 53015 a1119cf551e8
child 54147 97a8ff4e4ac9
     1.1 --- a/src/HOL/Power.thy	Sun Aug 18 17:00:10 2013 +0200
     1.2 +++ b/src/HOL/Power.thy	Sun Aug 18 18:49:45 2013 +0200
     1.3 @@ -74,11 +74,11 @@
     1.4    by (simp add: numeral_3_eq_3 mult_assoc)
     1.5  
     1.6  lemma power_even_eq:
     1.7 -  "a ^ (2*n) = (a ^ n) ^ 2"
     1.8 +  "a ^ (2 * n) = (a ^ n)\<^sup>2"
     1.9    by (subst mult_commute) (simp add: power_mult)
    1.10  
    1.11  lemma power_odd_eq:
    1.12 -  "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
    1.13 +  "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
    1.14    by (simp add: power_even_eq)
    1.15  
    1.16  lemma power_numeral_even: