# HG changeset patch
# User wenzelm
# Date 1004133501 -7200
# Node ID b10f1e8862f4000baa1f193abbb3ba633be46f6b
# Parent  381135c295effa84f86a64bc840d1cd414d84103
* 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*;

diff -r 381135c295ef -r b10f1e8862f4 NEWS
--- 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;