Email Gateway (Jan 09 2025 at 09:16): Email Gateway (Jan 09 2025 at 09:16):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi Larry,
I note that the theory Divides is being deprecated in favour of
Euclidean_Rings and that there are three separate news items seemingly
relating to aspects of this change. Could they be consolidated?
which entries are you referring to?
By full text search I only get
- Transitional theory "HOL.Divides" moved to "HOL-Library.Divides" and
supposed to be removed in a future release. Minor INCOMPATIBILITY.
Import "HOL-Library.Divides" and keep an eye on qualified names with prefix
"Divides" to ease transition.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Jan 30 2025 at 04:21 UTC