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