author | paulson |
Fri, 02 Nov 2001 17:55:24 +0100 | |
changeset 12018 | ec054019c910 |
parent 11701 | 3d51fbf81c17 |
child 14265 | 95b42e69436c |
permissions | -rw-r--r-- |
(* Title : HOL/Real/RealPow.thy ID : $Id$ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Description : Natural powers theory *) theory RealPow = RealAbs: (*belongs to theory RealAbs*) lemmas [arith_split] = abs_split instance real :: power .. primrec (realpow) realpow_0: "r ^ 0 = 1" realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" end