From: Jakub Kądziołka <firstname.lastname@example.org>
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
Is fixing typos like these possible, or would that be a compatibility
From: Lawrence Paulson <email@example.com>
Thanks for pointing this out. It will be taken care of.
Last updated: Dec 05 2021 at 23:19 UTC