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

Amine Chaieb 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 mailing list