NEWS
changeset 64523 49a29161d8ef
parent 64514 27914a4f8c70
child 64527 49708cffb98d
     1.1 --- a/NEWS	Wed Nov 23 20:55:58 2016 +0100
     1.2 +++ b/NEWS	Thu Nov 24 11:33:55 2016 +0100
     1.3 @@ -906,11 +906,12 @@
     1.4  support for monotonicity and continuity in chain-complete partial orders
     1.5  and about admissibility conditions for fixpoint inductions.
     1.6  
     1.7 -* Session HOL-Library: theory Polynomial contains also derivation of
     1.8 -polynomials but not gcd/lcm on polynomials over fields. This has been
     1.9 -moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave
    1.10 -way for a possible future different type class instantiation for
    1.11 -polynomials over factorial rings. INCOMPATIBILITY.
    1.12 +* Session HOL-Library: theory Library/Polynomial contains also
    1.13 +derivation of polynomials (formerly in Library/Poly_Deriv) but not
    1.14 +gcd/lcm on polynomials over fields. This has been moved to a separate
    1.15 +theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
    1.16 +future different type class instantiation for polynomials over factorial
    1.17 +rings. INCOMPATIBILITY.
    1.18  
    1.19  * Session HOL-Library: theory Sublist provides function "prefixes" with
    1.20  the following renaming