summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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