Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Typos in lemma names

view this post on Zulip Email Gateway (Nov 14 2020 at 11:41):

From: Jakub Kądziołka <>
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

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

Kind regards,
Jakub Kądziołka

view this post on Zulip Email Gateway (Nov 15 2020 at 14:02):

From: Lawrence Paulson <>
Thanks for pointing this out. It will be taken care of.

Last updated: Jan 25 2022 at 01:11 UTC