--- 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;