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;
wenzelm@9435
     1
(*  Title       : HOL/Real/RealPow.thy
paulson@7219
     2
    ID          : $Id$
paulson@7077
     3
    Author      : Jacques D. Fleuriot  
paulson@7077
     4
    Copyright   : 1998  University of Cambridge
paulson@7077
     5
    Description : Natural powers theory
paulson@7077
     6
paulson@7077
     7
*)
paulson@7077
     8
wenzelm@9435
     9
theory RealPow = RealAbs:
paulson@7077
    10
wenzelm@9435
    11
(*belongs to theory RealAbs*)
wenzelm@9435
    12
lemmas [arith_split] = abs_split
wenzelm@9435
    13
wenzelm@9435
    14
wenzelm@10309
    15
instance real :: power ..
paulson@7077
    16
wenzelm@8856
    17
primrec (realpow)
wenzelm@11701
    18
     realpow_0:   "r ^ 0       = Numeral1"
wenzelm@9435
    19
     realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
paulson@7077
    20
paulson@7077
    21
end