src/HOL/Power.thy

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