| changeset 7077 | 60b098bb8b8a |
| child 7219 | 4e3f386c2e37 |
| 7076:a30e024791c6 | 7077:60b098bb8b8a |
|---|---|
1 (* Title : RealPow.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Natural powers theory |
|
5 |
|
6 *) |
|
7 |
|
8 RealPow = WF_Rel + RealAbs + |
|
9 |
|
10 instance real :: {power} |
|
11 |
|
12 primrec |
|
13 realpow_0 "r ^ 0 = 1r" |
|
14 realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)" |
|
15 |
|
16 end |