Hi all,
just a few comments on my behalf.
>> 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.
Seems to make sense.
> Just one oddity in HOL-Algebra: It claims canonical theory names like>
> "Group", "Ring",
On 12/05/18 11:40, Lawrence Paulson wrote:
> 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
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
On 08/05/18 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
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
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
