NEWS
changeset 68647 f0d98441eff5
parent 68640 f15daa73ee32
child 68665 5820f0f379ae
     1.1 --- a/NEWS	Tue Jul 17 22:18:27 2018 +0100
     1.2 +++ b/NEWS	Wed Jul 18 11:47:05 2018 +0200
     1.3 @@ -231,9 +231,6 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* New proof method "real_asymp" to prove asymptotics or real-valued 
     1.8 -  functions (limits, "Big-O", etc.) automatically.
     1.9 -
    1.10  * Sledgehammer: bundled version of "vampire" (for non-commercial users)
    1.11  helps to avoid fragility of "remote_vampire" service.
    1.12  
    1.13 @@ -380,8 +377,8 @@
    1.14  * Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
    1.15  generator to generate code for algebraic types with lazy evaluation
    1.16  semantics even in call-by-value target languages. See the theories
    1.17 -HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for
    1.18 -some examples.
    1.19 +HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some
    1.20 +examples.
    1.21  
    1.22  * Theory HOL-Library.Landau_Symbols has been moved here from AFP.
    1.23  
    1.24 @@ -412,6 +409,9 @@
    1.25  Riemann mapping theorem, the Vitali covering theorem,
    1.26  change-of-variables results for integration and measures.
    1.27  
    1.28 +* Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics
    1.29 +or real-valued functions (limits, "Big-O", etc.) automatically.
    1.30 +
    1.31  * Session HOL-Types_To_Sets: more tool support (unoverload_type combines
    1.32  internalize_sorts and unoverload) and larger experimental application
    1.33  (type based linear algebra transferred to linear algebra on subspaces).