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é _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
