Email Gateway (Aug 22 2022 at 14:25): Email Gateway (Aug 22 2022 at 14:25):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Makarius wrote:
There are (at least) two theory files that have disappeared with no
corresponding NEWS entry:
~~/src/HOL/Number_Theory/UniqueFactorization.thy
one can import ~~/src/HOL/Number_Theory/Cong and Multiset instead
cf. 831816778409
~~/src/HOL/Library/Poly_Deriv.thy
it appears that the content has moved to Polynomial.thy
cf. 35a9e1cbb5b3
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 14:25):From: Manuel Eberl <eberlm@in.tum.de>
The former is my fault; that disappeared during my generalisation of the
concepts of primality and prime factorisation. There is a news entry on
that, but I concede that it does not specifically mention
UniqueFactorization.
I would actually suggest not to import "Cong" by itself, but to import
"Number_Theory".
Manuel
Email Gateway (Aug 22 2022 at 14:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Makarius,
the reported issue on Poly_Deriv.thy justifies a clarification of the
NEWS (see below).
Can you take care of this?
Thanks a lot,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 14:26):From: Makarius <makarius@sketis.net>
Can you send me a formal changeset (hg export)?
Makarius
signature.asc
Email Gateway (Aug 22 2022 at 14:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Attached.
news
signature.asc
Last updated: Apr 25 2024 at 08:20 UTC