[isabelle-dev] classes

[Clemens Ballarin]

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