[isabelle-dev] HOL-Algebra

[Manuel Eberl]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180508/c379d012/attachment-0002.html>