NEWS
changeset 64523 49a29161d8ef
parent 64514 27914a4f8c70
child 64527 49708cffb98d
equal deleted inserted replaced
64522:b66f8caf86b6 64523:49a29161d8ef
   904 
   904 
   905 * Session HOL-Library: theory Complete_Partial_Order2 provides reasoning
   905 * Session HOL-Library: theory Complete_Partial_Order2 provides reasoning
   906 support for monotonicity and continuity in chain-complete partial orders
   906 support for monotonicity and continuity in chain-complete partial orders
   907 and about admissibility conditions for fixpoint inductions.
   907 and about admissibility conditions for fixpoint inductions.
   908 
   908 
   909 * Session HOL-Library: theory Polynomial contains also derivation of
   909 * Session HOL-Library: theory Library/Polynomial contains also
   910 polynomials but not gcd/lcm on polynomials over fields. This has been
   910 derivation of polynomials (formerly in Library/Poly_Deriv) but not
   911 moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave
   911 gcd/lcm on polynomials over fields. This has been moved to a separate
   912 way for a possible future different type class instantiation for
   912 theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
   913 polynomials over factorial rings. INCOMPATIBILITY.
   913 future different type class instantiation for polynomials over factorial
       
   914 rings. INCOMPATIBILITY.
   914 
   915 
   915 * Session HOL-Library: theory Sublist provides function "prefixes" with
   916 * Session HOL-Library: theory Sublist provides function "prefixes" with
   916 the following renaming
   917 the following renaming
   917 
   918 
   918   prefixeq -> prefix
   919   prefixeq -> prefix