[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:


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.