Re: [isabelle] abelian_group




I do not say that this is not possible, but IMHO there are too many open
questions to tackle that on one step;  the existing algebraic type class
hierarchy is essential for the HOL bootstrap e.g. wrt. numeric types
without subtyping.

I was not suggesting to remove the type classes. In fact, I believe that they are much easier to use. What I was suggesting is much less ambitous: If HOL-Algebra is overhauled, make sure the locales stand in 1-1 correspondence with the classes. I agree with you that the dichotomy is necessary, but what isn't necessary but rather historical is that, e.g., naming conventions are incompatible. (Purely a usability issue, not a mathematical consideration.)

Best wishes,
Dominique.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.