wenzelm [Fri, 26 Oct 2001 23:58:21 +0200] rev 11952
* 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*;