Overloading of "^" requires new type class "power", with types "nat" and
"set" in that class. The operator itself is declared in Nat.thy

--- a/src/HOL/HOL.thy	Fri May 30 15:17:36 1997 +0200
+++ b/src/HOL/HOL.thy	Fri May 30 15:19:58 1997 +0200
@@ -66,12 +66,14 @@
 axclass
   times < term
 
+axclass
+  power < term
+
 consts
-  "+"           :: ['a::plus, 'a] => 'a             (infixl 65)
+  "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
   "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
   "*"           :: ['a::times, 'a] => 'a            (infixl 70)
-
-
+  (*See Nat.thy for "^"*)
 
 (** Additional concrete syntax **)
 

--- a/src/HOL/Nat.thy	Fri May 30 15:17:36 1997 +0200
+++ b/src/HOL/Nat.thy	Fri May 30 15:19:58 1997 +0200
@@ -10,4 +10,7 @@
 
 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
 
+consts
+  "^"           :: ['a::power,nat] => 'a            (infixr 80)
+
 end

--- a/src/HOL/RelPow.thy	Fri May 30 15:17:36 1997 +0200
+++ b/src/HOL/RelPow.thy	Fri May 30 15:19:58 1997 +0200
@@ -8,9 +8,6 @@
 
 RelPow = Nat +
 
-consts
-  "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100)
-
 primrec "op ^" nat
   "R^0 = id"
   "R^(Suc n) = R O (R^n)"

--- a/src/HOL/Set.thy	Fri May 30 15:17:36 1997 +0200
+++ b/src/HOL/Set.thy	Fri May 30 15:19:58 1997 +0200
@@ -16,7 +16,7 @@
   set :: (term) term
 
 instance
-  set :: (term) {ord, minus}
+  set :: (term) {ord, minus, power}
 
 consts
   "{}"          :: 'a set                           ("{}")