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



The former is my fault; that disappeared during my generalisation of the concepts of primality and prime factorisation. There is a news entry on that, but I concede that it does not specifically mention UniqueFactorization.

I would actually suggest not to import "Cong" by itself, but to import "Number_Theory".

Manuel



On 2016-11-22 12:39, Bertram Felgenhauer via Cl-isabelle-users wrote:
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





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