summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 18 Jul 2018 11:47:05 +0200 | |

changeset 68647 | f0d98441eff5 |

parent 68646 | 7dc9fe795dae |

child 68648 | 371e814af6f0 |

tuned;

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