1.1 --- a/src/HOL/Power.thy	Fri Oct 12 08:25:47 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Fri Oct 12 08:25:48 2007 +0200
     1.3 @@ -11,6 +11,9 @@
     1.4  imports Nat
     1.5  begin
     1.6  
     1.7 +class power = type +
     1.8 +  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
     1.9 +
    1.10  subsection{*Powers for Arbitrary Monoids*}
    1.11  
    1.12  class recpower = monoid_mult + power +