1.1 --- a/NEWS	Thu Nov 08 23:50:08 2001 +0100
     1.2 +++ b/NEWS	Thu Nov 08 23:52:56 2001 +0100
     1.3 @@ -89,6 +89,11 @@
     1.4  application: 'induct' method with proper rule statements in improper
     1.5  proof *scripts*;
     1.6  
     1.7 +* Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.)
     1.8 +now consider the syntactic context of assumptions, giving a better
     1.9 +chance to get type-inference of the arguments right (this is
    1.10 +especially important for locales);
    1.11 +
    1.12  * Provers: 'simplified' attribute may refer to explicit rules instead
    1.13  of full simplifier context; 'iff' attribute handles conditional rules;
    1.14  
    1.15 @@ -214,6 +219,10 @@
    1.16  * syntax: builtin parse translation for "_constify" turns valued
    1.17  tokens into AST constants;
    1.18  
    1.19 +* system: refrain from any attempt at filtering input streams; no
    1.20 +longer support ``8bit'' encoding of old isabelle font, instead proper
    1.21 +iso-latin characters may now be used;
    1.22 +
    1.23  * system: support Poly/ML 4.1.1 (now able to manage large heaps);
    1.24  
    1.25  * system: Proof General keywords specification is now part of the