* Provers: Simplifier.simproc(_i) now provide sane interface for
setting up simprocs;

--- a/NEWS	Tue Aug 06 11:22:05 2002 +0200
+++ b/NEWS	Tue Aug 06 11:24:27 2002 +0200
@@ -19,15 +19,18 @@
 parameters (as in CASL, for example); just specify something like
 ``var x + var y + struct M'' as import;
 
-* improved induct method: assumptions introduced by case "foo" are
-split into "foo.hyps" (from the rule) and "foo.prems" (from the goal
-statement); "foo" still refers to all facts collectively;
-
-* improved thms_containing: proper indexing of facts instead of raw
-theorems; check validity of results wrt. current name space; include
-local facts of proof configuration (also covers active locales); an
-optional limit for the number of printed facts may be given (the
-default is 40);
+* Pure: improved thms_containing: proper indexing of facts instead of
+raw theorems; check validity of results wrt. current name space;
+include local facts of proof configuration (also covers active
+locales); an optional limit for the number of printed facts may be
+given (the default is 40);
+
+* Provers: improved induct method: assumptions introduced by case
+"foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
+the goal statement); "foo" still refers to all facts collectively;
+
+* Provers: Simplifier.simproc(_i) now provide sane interface for
+setting up simprocs;
 
 
 *** HOL ***