* Pure: method 'atomize' presents local goal premises as object-level
statements (atomic meta-level propositions); setup controlled via
rewrite rules declarations of 'atomize' attribute; example
application: 'induct' method with proper rule statements in improper
proof *scripts*;

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