# HG changeset patch
# User paulson
# Date 864998398 -7200
# Node ID 5c5fdce3a4e4fd5001cd04631ca74e15672bd55b
# Parent  51ed014406fa4790a11702debb66d4af7eed0dd9
Overloading of "^" requires new type class "power", with types "nat" and
"set" in that class.  The operator itself is declared in Nat.thy

diff -r 51ed014406fa -r 5c5fdce3a4e4 src/HOL/HOL.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 **)
 
diff -r 51ed014406fa -r 5c5fdce3a4e4 src/HOL/Nat.thy
--- 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
diff -r 51ed014406fa -r 5c5fdce3a4e4 src/HOL/RelPow.thy
--- 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)"
diff -r 51ed014406fa -r 5c5fdce3a4e4 src/HOL/Set.thy
--- 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                           ("{}")