| changeset 68630 | c55f6f0b3854 |
| parent 68568 | cf01d04e94d7 |
| child 68640 | f15daa73ee32 |
--- a/NEWS Sun Jul 15 01:14:04 2018 +0100 +++ b/NEWS Sun Jul 15 14:46:57 2018 +0200 @@ -231,6 +231,9 @@ *** 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.