--- a/NEWS Sun Oct 08 22:28:20 2017 +0200
+++ b/NEWS Sun Oct 08 22:28:21 2017 +0200
@@ -44,6 +44,11 @@
higher-order quantifiers. An 'smt_explicit_application' option has been
added to control this. INCOMPATIBILITY.
+* Theory HOL-Computational_Algebra.Polynomial_Factorial does not
+provide instances of rat, real, complex as factorial rings etc.
+Import HOL-Computational_Algebra.Field_as_Ring explicitly in case of
+need. INCOMPATIBILITY.
+
* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.