| changeset 29608 | 564ea783ace8 |
| parent 28131 | 3130d7b3149d |
| child 29978 | 33df3c4eb629 |
| child 30240 | 5b25fee0362c |
| 29586:4f9803829625 | 29608:564ea783ace8 |
|---|---|
9 |
9 |
10 theory Power |
10 theory Power |
11 imports Nat |
11 imports Nat |
12 begin |
12 begin |
13 |
13 |
14 class power = type + |
14 class power = |
15 fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) |
15 fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) |
16 |
16 |
17 subsection{*Powers for Arbitrary Monoids*} |
17 subsection{*Powers for Arbitrary Monoids*} |
18 |
18 |
19 class recpower = monoid_mult + power + |
19 class recpower = monoid_mult + power + |