[isabelle-dev] class recpower and other classes...

[Amine Chaieb]

  this.  (IMHO the key point is that we have to stop to abuse to type
> system to achieve the same notation for different operations).

I don't see why the recpower is an "abuse" of the type system... If I 
want to use inside a class, the type is fixed and I see no problem...

This was not my point at least. I want(ed) to have merge point for the 
so many nice-looking classes, so that the interesting theorem can be 
proved inside the locale and not only inside axclasses.

Amine.