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.


isabelle-dev mailing list

Reply via email to