src/HOL/Power.thy
changeset 29608 564ea783ace8
parent 28131 3130d7b3149d
child 29978 33df3c4eb629
child 30240 5b25fee0362c
equal deleted inserted replaced
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 +