diff r 7dc9fe795dae r f0d98441eff5 NEWS
 a/NEWS Tue Jul 17 22:18:27 2018 +0100
+++ b/NEWS Wed Jul 18 11:47:05 2018 +0200
@@ 231,9 +231,6 @@
*** HOL ***
* New proof method "real_asymp" to prove asymptotics or realvalued
 functions (limits, "BigO", etc.) automatically.

* Sledgehammer: bundled version of "vampire" (for noncommercial users)
helps to avoid fragility of "remote_vampire" service.
@@ 380,8 +377,8 @@
* Theory HOLLibrary.Code_Lazy provides a new preprocessor for the code
generator to generate code for algebraic types with lazy evaluation
semantics even in callbyvalue target languages. See the theories
HOLex.Code_Lazy_Demo and HOLCodegenerator_Test.Code_Lazy_Test for
some examples.
+HOLex.Code_Lazy_Demo and HOLCodegenerator_Test.Code_Lazy_Test for some
+examples.
* Theory HOLLibrary.Landau_Symbols has been moved here from AFP.
@@ 412,6 +409,9 @@
Riemann mapping theorem, the Vitali covering theorem,
changeofvariables results for integration and measures.
+* Session HOLReal_Asymp: proof method "real_asymp" proves asymptotics
+or realvalued functions (limits, "BigO", etc.) automatically.
+
* Session HOLTypes_To_Sets: more tool support (unoverload_type combines
internalize_sorts and unoverload) and larger experimental application
(type based linear algebra transferred to linear algebra on subspaces).