[isabelle-dev] Isabelle2016-RC0: potential changes
Rene.Thiemann at uibk.ac.at
Mon Jan 11 09:57:21 CET 2016
there are some changes I would like to add for the upcoming release. It would be nice, if someone can integrate them:
- improved code equations for binomial coefficients and certain divmod-algorithms.
- change type in definition and lemmas about pderiv from real to arbitrary fields, or even more general, cf. lines starting with
(* TODO: inform Isabelle developers *) in http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Square_Free_Factorization.html
- change type of divides_degree from complex to 'a :: idom, cf beginning of
Moreover, everything of
can freely be moved from the AFP into the distribution, where I ask the developers to judge which parts
belong in the distribution and which are too specific, etc.
With best regards,
More information about the isabelle-dev