I added the efficient code equations for fact and binomial, and similar
ones for pochhammer and gbinomial.
I also adapted everything from Square_Free_Factorization and
Missing_Polynomial that seemed to be of general interest to me
(especially the generalisation of the type of pderiv).
I also noticed the ring_gcd instance for polynomials. Finalising the
changes to the GCD class hierarchy and updating the AFP entries that
rely on half-finished versions of this change (such as Echelon_Form) is
something that I should probably take care of soon, but definitely not
before the 2016 release – hopefully before the 2017 one.
Manuel
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
