| changeset 9013 | 9dd0274f76af |
| parent 8856 | 435187ffc64e |
| child 9435 | c3a13a7d4424 |
| 9012:d1bd2144ab5d | 9013:9dd0274f76af |
|---|---|
9 RealPow = RealAbs + |
9 RealPow = RealAbs + |
10 |
10 |
11 instance real :: {power} |
11 instance real :: {power} |
12 |
12 |
13 primrec (realpow) |
13 primrec (realpow) |
14 realpow_0 "r ^ 0 = 1r" |
14 realpow_0 "r ^ 0 = #1" |
15 realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)" |
15 realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)" |
16 |
16 |
17 end |
17 end |