I have a student who was going to formalise things about fields and field extensions. Does that clash with your work in any way?
In any case, we should definitely coordinate our efforts here to avoid duplication of work. Manuel On 2018-05-08 13:49, Lawrence Paulson wrote: > I have two interns from École Polytechnique. They have been going over > HOL-Algebra and Group-Ring-Module, providing new proofs of the best results > in the latter and tidying up some messy proofs in the former, as well. They > are also systematising the chaotic naming conventions that they found there. > So there will be big changes to HOL-Algebra in the coming weeks. This is an > early warning in case anybody else wants to work on this directory. > > Larry > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
