[isabelle-dev] class recpower and other classes...
chaieb at in.tum.de
Tue Nov 6 17:02:27 CET 2007
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.
More information about the isabelle-dev