| changeset 11868 | 56db9f3a6b3e |
| parent 11701 | 3d51fbf81c17 |
| child 14259 | 79f7d3451b1e |
| 11867:76401b2ee871 | 11868:56db9f3a6b3e |
|---|---|
10 |
10 |
11 instance |
11 instance |
12 int :: {power} |
12 int :: {power} |
13 |
13 |
14 primrec |
14 primrec |
15 power_0 "p ^ 0 = Numeral1" |
15 power_0 "p ^ 0 = 1" |
16 power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)" |
16 power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)" |
17 |
17 |
18 end |
18 end |