--- a/NEWS Wed Aug 07 20:11:07 2002 +0200
+++ b/NEWS Thu Aug 08 23:42:10 2002 +0200
@@ -29,9 +29,6 @@
"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 ***
@@ -54,6 +51,18 @@
takes ~= in premises into account (by performing a case split);
+*** ML ***
+
+* Pure: Tactic.prove provides sane interface for internal proofs;
+omits the infamous "standard" operation, so this is more appropriate
+than prove_goalw_cterm in many situations (e.g. in simprocs);
+
+* Pure: improved error reporting of simprocs;
+
+* Provers: Simplifier.simproc(_i) provides sane interface for setting
+up simprocs;
+
+
New in Isabelle2002 (March 2002)
--------------------------------