I suggest that those of us in M do not start an email discussion but meet in person to discuss this.
Tobias Amine Chaieb schrieb: > The class recpower is very unfortunate. I suggest to remove it and > replace it by definitions inside the locale/class (The axioms *are* a > recursive function definition). > > The problem with the actual structure of classes is that many classes > have been separated (which is nice for separation of concepts) but now > we need to merge almost any two interesting classes into one in order to > prove theorems in the locale and not on the axclass level, since it is > not possible to do the following: > > lemma (in ring + recpower) ... > > as soon as you want a theorem about power in rings, where power is > something very natural in terms of multiplication... > > any suggestions, thoughts? > > I also suggest the introduction of several "join" classes such as > (semi)ring/field + division_by_zero > ring + characteristic_zero > and many other useful classes, we use "almost daily". Is it thinkable to > have such things in HOL or should I just rebuild the Ring_and_Field > theory as I need it? > > Amine. > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
