sligthly more interpunctation and qualification
authorhaftmann
Thu Feb 21 09:15:06 2019 +0000 (7 months ago)
changeset 6982874d673b7d40e
parent 69827 7c0a2ab90786
child 69829 3bfa28b3a5b2
sligthly more interpunctation and qualification
NEWS
     1.1 --- a/NEWS	Thu Feb 21 09:15:06 2019 +0000
     1.2 +++ b/NEWS	Thu Feb 21 09:15:06 2019 +0000
     1.3 @@ -88,17 +88,18 @@
     1.4  *** HOL ***
     1.5  
     1.6  * Formal Laurent series and overhaul of Formal power series 
     1.7 -in HOL-Computational_Algebra
     1.8 -
     1.9 -* Exponentiation by squaring in HOL-Library; used for computing powers
    1.10 -in monoid_mult and modular exponentiation in HOL-Number_Theory
    1.11 -
    1.12 -* more material on residue rings in HOL-Number_Theory:
    1.13 -Carmichael's function, primitive roots, more properties for "ord"
    1.14 -
    1.15 -* the functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
    1.16 +in session HOL-Computational_Algebra.
    1.17 +
    1.18 +* Exponentiation by squaring in session HOL-Library; used for computing
    1.19 +powers in class monoid_mult and modular exponentiation in session
    1.20 +HOL-Number_Theory.
    1.21 +
    1.22 +* More material on residue rings in session HOL-Number_Theory:
    1.23 +Carmichael's function, primitive roots, more properties for "ord".
    1.24 +
    1.25 +* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
    1.26  (not the corresponding binding operators) now have the same precedence
    1.27 -as any other prefix function symbol.
    1.28 +as any other prefix function symbol.  Minor INCOMPATIBILITY.
    1.29  
    1.30  * Slightly more conventional naming schema in structure Inductive.
    1.31  Minor INCOMPATIBILITY.