src/HOL/Real/RealPow.thy
author wenzelm
Fri Oct 05 21:52:39 2001 +0200 (2001-10-05)
changeset 11701 3d51fbf81c17
parent 10309 a7f961fb62c6
child 12018 ec054019c910
permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
     1 (*  Title       : HOL/Real/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 theory RealPow = RealAbs:
    10 
    11 (*belongs to theory RealAbs*)
    12 lemmas [arith_split] = abs_split
    13 
    14 
    15 instance real :: power ..
    16 
    17 primrec (realpow)
    18      realpow_0:   "r ^ 0       = Numeral1"
    19      realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
    20 
    21 end