NEWS
changeset 14257 a7ef3f7588c5
parent 14255 e6e3e3f0deed
child 14283 516358ca7b42
     1.1 --- a/NEWS	Wed Nov 12 10:58:23 2003 +0100
     1.2 +++ b/NEWS	Fri Nov 14 14:35:55 2003 +0100
     1.3 @@ -41,6 +41,11 @@
     1.4      longer be enclosed in quotes.  Instead, precede variable name with `?'.
     1.5      This is consistent with the instantiation attribute "where".
     1.6  
     1.7 +* Attributes "where" and "of":
     1.8 +  Now take type variables of instantiated theorem into account when reading
     1.9 +  the instantiation string.  This fixes a bug that caused instantiated
    1.10 +  theorems to have too special types in some circumstances.
    1.11 +
    1.12  * Locales:
    1.13    - Goal statements involving the context element "includes" no longer
    1.14      generate theorems with internal delta predicates (those ending on