Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Typos in lemma names

Email Gateway (Nov 14 2020 at 11:41):

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

Email Gateway (Nov 15 2020 at 14:02):

From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for pointing this out. It will be taken care of.
Larry

Last updated: Jan 04 2025 at 20:18 UTC