changeset 14283 | 516358ca7b42 |
parent 14257 | a7ef3f7588c5 |
child 14285 | 92ed032e83a1 |
--- 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