>> This would have not been possible without merging some classes. > > Which? > Just these:
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 class recpower_comm_semiring_1 = recpower + comm_semiring_1 class recpower_comm_ring_1 = recpower + comm_ring_1 subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by unfold_locales class recpower_idom = recpower + idom subclass (in recpower_idom) recpower_comm_ring_1 by unfold_locales class idom0 = idom + ring_char_0 class recpower_idom0 = recpower + idom0 subclass (in recpower_idom0) recpower_idom by unfold_locales subclass (in idom0) comm_ring_1 by unfold_locales > And what exactly does "merging" mean? Do you just add a new class which > "inherits" from both existing classes? Then it would be a conservative > extension...? Yes, see above. > > When you changed things locally, what effects did it have on other theories? > I just added these at the beginning of my theory, so I have no idea what would happen if they were in HOL. I also did not try to do more than needed, just what I needed to make Polynomials local. > I think I like this future, but I still agree with Makarius: Unless > there is something severely broken in the current state of affairs, we > should really be disciplined and wait for the release first. > The release Idea (as far as I understood Makarius) is that the system should "freeze" for a couple of weeks while we are *using* it and report our experience. That's all I did, just report (while bemoaning, I must admit). I leave it to others to decide if this is important to change now of not. I myself think it quite manageable to fix in a reasonable time but I also fully understand that this release-preparation time is critical. Regardless of release, there are several subtle issues with classes which need to be fixed. > And in fact your proposal is more of the visionary kind than of the > "fixes a pressing problem" kind, isn't it? It is not really a pressing problem. The other problem (parsing/type inference) I reported locally on the TUM list, is in my opinion pressing -- Thanks for Makarius who fixed it. Amine.