1.1 --- a/src/HOL/Power.thy	Fri Mar 02 15:43:20 2007 +0100
     1.2 +++ b/src/HOL/Power.thy	Fri Mar 02 15:43:21 2007 +0100
     1.3 @@ -13,9 +13,9 @@
     1.4  
     1.5  subsection{*Powers for Arbitrary Monoids*}
     1.6  
     1.7 -axclass recpower \<subseteq> monoid_mult, power
     1.8 -  power_0 [simp]: "a ^ 0       = 1"
     1.9 -  power_Suc:      "a ^ (Suc n) = a * (a ^ n)"
    1.10 +class recpower = monoid_mult + power +
    1.11 +  assumes power_0 [simp]: "a \<^loc>^ 0       = \<^loc>1"
    1.12 +  assumes power_Suc:      "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)"
    1.13  
    1.14  lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
    1.15  by (simp add: power_Suc)