src/HOL/Nat.thy
changeset 3370 5c5fdce3a4e4
parent 2608 450c9b682a92
child 4104 84433b1ab826
     1.1 --- a/src/HOL/Nat.thy	Fri May 30 15:17:36 1997 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri May 30 15:19:58 1997 +0200
     1.3 @@ -10,4 +10,7 @@
     1.4  
     1.5  instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
     1.6  
     1.7 +consts
     1.8 +  "^"           :: ['a::power,nat] => 'a            (infixr 80)
     1.9 +
    1.10  end