# HG changeset patch
# User wenzelm
# Date 973879471 -3600
# Node ID b100e8d2c355893cfc757c1ff52cf9a79958facd
# Parent  6ea4735c39552cff28d0baaf289d9ba0669bca61
added axclass power (from HOL.thy);

diff -r 6ea4735c3955 -r b100e8d2c355 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 * *)