[isabelle-dev] Isabelle2016-RC0: potential changes

[Manuel Eberl]

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