src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Fri Nov 10 19:03:55 2000 +0100
+++ b/src/HOL/Nat.thy	Fri Nov 10 19:04:31 2000 +0100
@@ -18,8 +18,10 @@
 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
 instance nat :: linorder (nat_le_linear)
 
+axclass power < term
+
 consts
-  "^"           :: ['a::power,nat] => 'a            (infixr 80)
+  power :: ['a::power, nat] => 'a            (infixr "^" 80)
 
 
 (* arithmetic operators + - and * *)