NEWS
changeset 66805 274b4edca859
parent 66804 3f9bb52082c4
child 66826 0d60d2118544
     1.1 --- a/NEWS	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/NEWS	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -44,6 +44,11 @@
     1.4      higher-order quantifiers. An 'smt_explicit_application' option has been
     1.5      added to control this. INCOMPATIBILITY.
     1.6  
     1.7 +* Theory HOL-Computational_Algebra.Polynomial_Factorial does not
     1.8 +provide instances of rat, real, complex as factorial rings etc.
     1.9 +Import HOL-Computational_Algebra.Field_as_Ring explicitly in case of
    1.10 +need. INCOMPATIBILITY.
    1.11 +
    1.12  * Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
    1.13  with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
    1.14