| changeset 12018 | ec054019c910 |
| parent 11701 | 3d51fbf81c17 |
| child 14265 | 95b42e69436c |
| 12017:78b8f9e13300 | 12018:ec054019c910 |
|---|---|
13 |
13 |
14 |
14 |
15 instance real :: power .. |
15 instance real :: power .. |
16 |
16 |
17 primrec (realpow) |
17 primrec (realpow) |
18 realpow_0: "r ^ 0 = Numeral1" |
18 realpow_0: "r ^ 0 = 1" |
19 realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" |
19 realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" |
20 |
20 |
21 end |
21 end |