[isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

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
  http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_Polynomial.html

Moreover, everything of

http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_*
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Missing_*

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,
René