author | wenzelm |
Tue, 25 Jul 2000 00:03:39 +0200 | |
changeset 9435 | c3a13a7d4424 |
parent 9013 | 9dd0274f76af |
child 10309 | a7f961fb62c6 |
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 by intro_classes primrec (realpow) realpow_0: "r ^ 0 = #1" realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" end