summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 68647 | f0d98441eff5 |

parent 68640 | f15daa73ee32 |

child 68661 | 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).