1.1 --- a/NEWS	Fri Oct 26 23:17:49 2001 +0200
     1.2 +++ b/NEWS	Fri Oct 26 23:58:21 2001 +0200
     1.3 @@ -58,6 +58,12 @@
     1.4  bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
     1.5  supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
     1.6  
     1.7 +* Pure: method 'atomize' presents local goal premises as object-level
     1.8 +statements (atomic meta-level propositions); setup controlled via
     1.9 +rewrite rules declarations of 'atomize' attribute; example
    1.10 +application: 'induct' method with proper rule statements in improper
    1.11 +proof *scripts*;
    1.12 +
    1.13  * Provers: 'simplified' attribute may refer to explicit rules instead
    1.14  of full simplifier context; 'iff' attribute handles conditional rules;
    1.15