author | kleing |
Sat, 06 Dec 2003 07:52:17 +0100 | |
changeset 14283 | 516358ca7b42 |
parent 14282 | b23f028c1651 |
child 14284 | f1abe67c448a |
--- a/NEWS Sat Dec 06 07:50:01 2003 +0100 +++ b/NEWS Sat Dec 06 07:52:17 2003 +0100 @@ -46,6 +46,9 @@ the instantiation string. This fixes a bug that caused instantiated theorems to have too special types in some circumstances. +* Calculation commands "moreover" and "also": + Do not reset facts ("this") any more. + * Locales: - Goal statements involving the context element "includes" no longer generate theorems with internal delta predicates (those ending on