| changeset 42154 | 478bdcea240a |
| parent 35316 | 870dfea4f9c0 |
| child 58860 | fee7cfa69c50 |
| 42153:fa108629d132 | 42154:478bdcea240a |
|---|---|
88 c := c*a; b := b - 1 |
88 c := c*a; b := b - 1 |
89 OD |
89 OD |
90 {c = A^B}" |
90 {c = A^B}" |
91 apply vcg_simp |
91 apply vcg_simp |
92 apply(case_tac "b") |
92 apply(case_tac "b") |
93 apply(simp add: mod_less) |
93 apply simp |
94 apply simp |
94 apply simp |
95 done |
95 done |
96 |
96 |
97 (** Factorial **) |
97 (** Factorial **) |
98 |
98 |