equal
deleted
inserted
replaced
15 primrec (realpow) |
15 primrec (realpow) |
16 realpow_0: "r ^ 0 = 1" |
16 realpow_0: "r ^ 0 = 1" |
17 realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" |
17 realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" |
18 |
18 |
19 |
19 |
20 instance real :: ringpower |
20 instance real :: recpower |
21 proof |
21 proof |
22 fix z :: real |
22 fix z :: real |
23 fix n :: nat |
23 fix n :: nat |
24 show "z^0 = 1" by simp |
24 show "z^0 = 1" by simp |
25 show "z^(Suc n) = z * (z^n)" by simp |
25 show "z^(Suc n) = z * (z^n)" by simp |