Stream: General

Topic: Lemmas about mod division qualified in RC2024

view this post on Zulip Stepan Holub (May 07 2024 at 08:34):

I use lemma pos_mod_conj from HOL/Divides.thy, and it is part of a group that became qualified, hence not accessible in the Release Canidate 2024. Is there any explanation for this?

view this post on Zulip Mathias Fleury (May 07 2024 at 08:36):

qualified just mean that you have to use the long name Divides.XXX instead of XXX

view this post on Zulip Stepan Holub (May 07 2024 at 08:38):

Thanks, very good. Anyway, what may be the reason for that change? Some naming conflict, I guess.

view this post on Zulip Mathias Fleury (May 07 2024 at 08:51):

From the change, I think that those lemmas are supposed to be only relevant for Code_Numeral and not for general usage

view this post on Zulip Stepan Holub (May 07 2024 at 09:13):

I can see now that the deprecation is part of a generalization process leading from HOL/Divides to HOL/Euclidean_Rings.

Last updated: Dec 21 2024 at 12:33 UTC