Hi Amine, I quite agree that ^ should be a definition, in a suitable multiplicative semigroup/monoid preferably. But since in the current setup ^ is overloaded so it can also be used for any other operation this might be problematic.
> class recpower_semiring = semiring + recpower > class recpower_semiring_1 = semiring_1 + recpower > class recpower_semiring_0 = semiring_0 + recpower > class recpower_ring = ring + recpower > class recpower_ring_1 = ring_1 + recpower > subclass (in recpower_ring_1) recpower_ring by unfold_locales > subclass (in recpower_ring_1) recpower_ring by unfold_locales > ... These extensions are quite natural and shouldn't cause any harm. What speaks against putting them into Isabelle2007 is that if in the end we decide to put ^ into, say semiring, it might be a bit awkward to withdraw the recpower_ classes in a later release. Clemens