1.1 --- a/src/HOL/Power.thy	Fri Mar 05 15:26:04 2004 +0100
     1.2 +++ b/src/HOL/Power.thy	Fri Mar 05 15:26:14 2004 +0100
     1.3 @@ -171,13 +171,13 @@
     1.4  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
     1.5  
     1.6  lemma power_divide: 
     1.7 -    "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)"
     1.8 +    "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n / b ^ n)"
     1.9  apply (case_tac "b=0", simp add: power_0_left)
    1.10  apply (rule nonzero_power_divide) 
    1.11  apply assumption 
    1.12  done
    1.13  
    1.14 -lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
    1.15 +lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_ring,ringpower}) ^ n"
    1.16  apply (induct_tac "n")
    1.17  apply (auto simp add: power_Suc abs_mult)
    1.18  done
    1.19 @@ -301,8 +301,7 @@
    1.20    
    1.21  instance nat :: ringpower
    1.22  proof
    1.23 -  fix z :: nat
    1.24 -  fix n :: nat
    1.25 +  fix z n :: nat
    1.26    show "z^0 = 1" by simp
    1.27    show "z^(Suc n) = z * (z^n)" by simp
    1.28  qed