* Isar/Provers: 'simp' method now supports 'cong' modifiers;
* Provers: Simplifier.easy_setup;
tuned;

--- a/NEWS	Mon Aug 28 20:33:23 2000 +0200
+++ b/NEWS	Tue Aug 29 00:52:57 2000 +0200
@@ -152,6 +152,8 @@
 * Pure: theory command 'method_setup' provides a simple interface for
 definining proof methods in ML;
 
+* Provers: 'simp' method now supports 'cong' modifiers;
+
 * Provers: hypsubst support; also plain subst and symmetric attribute
 (the latter supercedes [RS sym]);
 
@@ -313,18 +315,22 @@
 
 *** General ***
 
-* blast(_tac) now handles actual object-logic rules as assumptions;
-note that auto(_tac) uses blast(_tac) internally, too;
+* Provers: blast(_tac) now handles actual object-logic rules as
+assumptions; note that auto(_tac) uses blast(_tac) internally as well;
 
-* AST translation rules no longer require constant head on LHS;
+* Provers: Simplifier.easy_setup provides a fast path to basic
+Simplifier setup for new object-logics;
+
+* Pure: AST translation rules no longer require constant head on LHS;
 
-* improved name spaces: ambiguous output is qualified; support for
-hiding of names;
+* Pure: improved name spaces: ambiguous output is qualified; support
+for hiding of names;
 
-* compression of ML heaps images may now be controlled via -c option
-of isabelle and isatool usedir (currently only observed by Poly/ML);
+* system: compression of ML heaps images may now be controlled via -c
+option of isabelle and isatool usedir (currently only observed by
+Poly/ML);
 
-* provide TAGS file for Isabelle sources;
+* system: provide TAGS file for Isabelle sources;
 
 * settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and
 XSYMBOL_HOME; no longer need to do manual configuration in most