tuned whitespace;
authorwenzelm
Wed Oct 11 20:57:12 2017 +0200 (19 months ago)
changeset 668440746d4781674
parent 66843 be08a7691c62
child 66845 6847eb01ae47
tuned whitespace;
NEWS
     1.1 --- a/NEWS	Wed Oct 11 20:55:11 2017 +0200
     1.2 +++ b/NEWS	Wed Oct 11 20:57:12 2017 +0200
     1.3 @@ -40,26 +40,29 @@
     1.4  * SMT module:
     1.5    - The 'smt_oracle' option is now necessary when using the 'smt' method
     1.6      with a solver other than Z3. INCOMPATIBILITY.
     1.7 -  - The encoding to first-order logic is now more complete in the presence of
     1.8 -    higher-order quantifiers. An 'smt_explicit_application' option has been
     1.9 -    added to control this. INCOMPATIBILITY.
    1.10 -
    1.11 -* Theory HOL-Computational_Algebra.Polynomial_Factorial does not
    1.12 -provide instances of rat, real, complex as factorial rings etc.
    1.13 -Import HOL-Computational_Algebra.Field_as_Ring explicitly in case of
    1.14 -need. INCOMPATIBILITY.
    1.15 -
    1.16 -* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
    1.17 -with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
    1.18 +  - The encoding to first-order logic is now more complete in the
    1.19 +    presence of higher-order quantifiers. An 'smt_explicit_application'
    1.20 +    option has been added to control this. INCOMPATIBILITY.
    1.21 +
    1.22 +* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
    1.23 +instances of rat, real, complex as factorial rings etc. Import
    1.24 +HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
    1.25 +INCOMPATIBILITY.
    1.26 +
    1.27 +* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid
    1.28 +clash with fact mod_mult_self4 (on more generic semirings).
    1.29 +INCOMPATIBILITY.
    1.30  
    1.31  * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
    1.32 -sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes
    1.33 -on interpretation of abstract locales. INCOMPATIBILITY.
    1.34 +sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
    1.35 +interpretation of abstract locales. INCOMPATIBILITY.
    1.36  
    1.37  * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
    1.38  INCOMPATIBILITY.
    1.39  
    1.40 -* Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
    1.41 +* Session HOL-Analysis: Moebius functions and the Riemann mapping
    1.42 +theorem.
    1.43 +
    1.44  
    1.45  *** System ***
    1.46