--- 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