src/HOL/Real/RealPow.thy
author fleuriot
Thu Jun 01 11:22:27 2000 +0200 (2000-06-01)
changeset 9013 9dd0274f76af
parent 8856 435187ffc64e
child 9435 c3a13a7d4424
permissions -rw-r--r--
Updated files to remove 0r and 1r from theorems in descendant theories
of RealBin. Some new theorems added.
     1 (*  Title       : RealPow.thy
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot  
     4     Copyright   : 1998  University of Cambridge
     5     Description : Natural powers theory
     6 
     7 *)
     8 
     9 RealPow = RealAbs +
    10 
    11 instance real :: {power}
    12 
    13 primrec (realpow)
    14      realpow_0   "r ^ 0       = #1"
    15      realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
    16 
    17 end