[isabelle] Notice of proposed changes to number theory libraries



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.