# HG changeset patch
# User wenzelm
# Date 1531907225 -7200
# Node ID f0d98441eff5d887b09ea10586dfb3dc926c5249
# Parent  7dc9fe795daea31b7d817f9a76f5877fec8c621d
tuned;

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 real-valued 
-  functions (limits, "Big-O", etc.) automatically.
-
 * Sledgehammer: bundled version of "vampire" (for non-commercial users)
 helps to avoid fragility of "remote_vampire" service.
 
@@ -380,8 +377,8 @@
 * Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
 generator to generate code for algebraic types with lazy evaluation
 semantics even in call-by-value target languages. See the theories
-HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for
-some examples.
+HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some
+examples.
 
 * Theory HOL-Library.Landau_Symbols has been moved here from AFP.
 
@@ -412,6 +409,9 @@
 Riemann mapping theorem, the Vitali covering theorem,
 change-of-variables results for integration and measures.
 
+* Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics
+or real-valued functions (limits, "Big-O", etc.) automatically.
+
 * Session HOL-Types_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).