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



Attached.

Am 24.11.2016 um 11:25 schrieb Makarius:
> On 24/11/16 10:56, Florian Haftmann wrote:
>> Hi Makarius,
>>
>> the reported issue on Poly_Deriv.thy justifies a clarification of the
>> NEWS (see below).
>>
>> Can you take care of this?
>>
>>> diff -r 1aef5a0e18d7 NEWS
> 
> Can you send me a formal changeset (hg export)?
> 
> 
> 	Makarius
> 
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# User haftmann
# Date 1479983635 -3600
#      Thu Nov 24 11:33:55 2016 +0100
# Node ID b210b426648992ad66584f7e03e02cc309d93d79
# Parent  1aef5a0e18d7a970d804fba80fc66585c76b8de1
clarified NEWS concerning Library/Poly_Deriv

diff -r 1aef5a0e18d7 -r b210b4266489 NEWS
--- a/NEWS	Wed Nov 23 16:15:17 2016 +0100
+++ b/NEWS	Thu Nov 24 11:33:55 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
+rings. INCOMPATIBILITY.
 
 * Session HOL-Library: theory Sublist provides function "prefixes" with
 the following renaming

Attachment: signature.asc
Description: OpenPGP digital signature



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