I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are ancient. They desperately need updating and streamlining.
We’ve decided that Group-Ring-Module is irremediable, and are using it only as a list of useful results that need to be done again. Larry > On 11 May 2018, at 23:40, Makarius <makar...@sketis.net> wrote: > > Is the chaotic naming in Group-Ring-Module or HOL-Algebra? According to > my information, Clemens Ballarin has taken great care about HOL-Algebra > over many years (even with contributions by students). >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
