added axclass power (from HOL.thy);
authorwenzelm
Fri Nov 10 19:04:31 2000 +0100 (2000-11-10)
changeset 10435b100e8d2c355
parent 10434 6ea4735c3955
child 10436 98c421dd5972
added axclass power (from HOL.thy);
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Fri Nov 10 19:03:55 2000 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Nov 10 19:04:31 2000 +0100
     1.3 @@ -18,8 +18,10 @@
     1.4  instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
     1.5  instance nat :: linorder (nat_le_linear)
     1.6  
     1.7 +axclass power < term
     1.8 +
     1.9  consts
    1.10 -  "^"           :: ['a::power,nat] => 'a            (infixr 80)
    1.11 +  power :: ['a::power, nat] => 'a            (infixr "^" 80)
    1.12  
    1.13  
    1.14  (* arithmetic operators + - and * *)