--- a/NEWS Sun Dec 07 16:30:06 2003 +0100
+++ b/NEWS Wed Dec 10 14:27:50 2003 +0100
@@ -42,9 +42,10 @@
This is consistent with the instantiation attribute "where".
* Attributes "where" and "of":
- Now take type variables of instantiated theorem into account when reading
- the instantiation string. This fixes a bug that caused instantiated
- theorems to have too special types in some circumstances.
+ - Now take type variables of instantiated theorem into account when reading
+ the instantiation string. This fixes a bug that caused instantiated
+ theorems to have too special types in some circumstances.
+ - "where" permits explicit instantiations of type variables.
* Calculation commands "moreover" and "also":
Do not reset facts ("this") any more.