Email Gateway (Aug 19 2022 at 13:23): Email Gateway (Aug 19 2022 at 13:23):From: Lawrence Paulson <lp15@cam.ac.uk>
We are planning to consolidate some of Isabelle’s number theory libraries, and warning users in advance in case any compatibility issues arise.
We currently have overlapping material in the following places:
HOL/Library/Binomial.thy
HOL/Number_Theory
HOL/Old_Number_Theory
We would hope, ultimately, end up with nothing but HOL/Number_Theory. Meanwhile, some of the experimental material in HOL/Number_Theory will be going away. The availability of implicit conversions from natural numbers to integers reduces the need to overload certain primitives, and we will go back to using Suc instead of n+1 for induction and recursion there.
Interested users will be able to follow these changes using development snapshots. The theory Library/Binomial.thy is likely to be deleted very soon, having already been combined with the theory of the same name in directory Number_Theory.
Larry Paulson
Last updated: Apr 20 2024 at 12:26 UTC