(*  Title       : RealPow.thy
    ID          : $Id: RealPow.thy,v 1.2 1999/08/16 16:41:44 paulson Exp $
    Author      : Jacques D. Fleuriot  
    Copyright   : 1998  University of Cambridge
    Description : Natural powers theory

*)

RealPow = WF_Rel + RealAbs + 

instance real :: {power}

primrec
     realpow_0   "r ^ 0       = 1r"
     realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"

end