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
