NEWS
changeset 14285 92ed032e83a1
parent 14283 516358ca7b42
child 14333 14f29eb097a3
     1.1 --- a/NEWS	Sun Dec 07 16:30:06 2003 +0100
     1.2 +++ b/NEWS	Wed Dec 10 14:27:50 2003 +0100
     1.3 @@ -42,9 +42,10 @@
     1.4      This is consistent with the instantiation attribute "where".
     1.5  
     1.6  * Attributes "where" and "of":
     1.7 -  Now take type variables of instantiated theorem into account when reading
     1.8 -  the instantiation string.  This fixes a bug that caused instantiated
     1.9 -  theorems to have too special types in some circumstances.
    1.10 +  - Now take type variables of instantiated theorem into account when reading
    1.11 +    the instantiation string.  This fixes a bug that caused instantiated
    1.12 +    theorems to have too special types in some circumstances.
    1.13 +  - "where" permits explicit instantiations of type variables.
    1.14  
    1.15  * Calculation commands "moreover" and "also":
    1.16    Do not reset facts ("this") any more.