| changeset 11701 | 3d51fbf81c17 |
| parent 9509 | 0f3ee1f89ca8 |
| child 11868 | 56db9f3a6b3e |
| 11700:a0e6bda62b7b | 11701:3d51fbf81c17 |
|---|---|
10 |
10 |
11 instance |
11 instance |
12 int :: {power} |
12 int :: {power} |
13 |
13 |
14 primrec |
14 primrec |
15 power_0 "p ^ 0 = #1" |
15 power_0 "p ^ 0 = Numeral1" |
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 |