From: Jakub Kądziołka <kuba@kadziolka.net>

Good evening,

I've just noticed that a typo in the name of

HOL.Divides.zmod_trival_iff - I would expect it to be called

zmod_trivial_iff (note the additional i in 'trivial').

A quick code grep shows that the same mistake is also present, apart

from some comments, in

HOL-Computational_Algebra.Polynomial.is_unit_monom_trival.

Is fixing typos like these possible, or would that be a compatibility

problem?

Kind regards,

Jakub Kądziołka

From: Lawrence Paulson <lp15@cam.ac.uk>

Thanks for pointing this out. It will be taken care of.

Larry

Last updated: Jan 25 2022 at 01:11 UTC