[isabelle-dev] Isabelle2016-RC0: potential changes

Thiemann, Rene Rene.Thiemann at uibk.ac.at
Mon Jan 11 09:57:21 CET 2016

Dear all,

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.

  (cf. http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html)

- 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 mailing list