Re: [isabelle] Isabelle2016-1-RC3 removed theories

Hi Makarius,

the reported issue on Poly_Deriv.thy justifies a clarification of the
NEWS (see below).

Can you take care of this?

Thanks a lot,

> diff -r 1aef5a0e18d7 NEWS
> --- a/NEWS	Wed Nov 23 16:15:17 2016 +0100
> +++ b/NEWS	Thu Nov 24 10:54:53 2016 +0100
> @@ -906,11 +906,12 @@
>  support for monotonicity and continuity in chain-complete partial orders
>  and about admissibility conditions for fixpoint inductions.
> -* Session HOL-Library: theory Polynomial contains also derivation of
> -polynomials but not gcd/lcm on polynomials over fields. This has been
> -moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave
> -way for a possible future different type class instantiation for
> -polynomials over factorial rings. INCOMPATIBILITY.
> +* Session HOL-Library: theory Library/Polynomial contains also
> +derivation of polynomials (formerly in Library/Poly_Deriv) but not
> +gcd/lcm on polynomials over fields. This has been moved to a separate
> +theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
> +future different type class instantiation for polynomials over factorial
>  * Session HOL-Library: theory Sublist provides function "prefixes" with
>  the following renaming

Am 22.11.2016 um 12:39 schrieb Bertram Felgenhauer via Cl-isabelle-users:
> Makarius wrote:
>> At this stage, Isabelle release candidates are already sufficiently
>> consolidated to be ready for everyday use. Adapting your applications
>> now gives a unique chance for feedback before the release is finalized.
> There are (at least) two theory files that have disappeared with no
> corresponding NEWS entry:
> - ~~/src/HOL/Number_Theory/UniqueFactorization.thy
>   one can import ~~/src/HOL/Number_Theory/Cong and Multiset instead
>   cf. 831816778409
> - ~~/src/HOL/Library/Poly_Deriv.thy
>   it appears that the content has moved to Polynomial.thy
>   cf. 35a9e1cbb5b3
> Cheers,
> Bertram


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.