# HG changeset patch
# User wenzelm
# Date 1028842930 -7200
# Node ID 9cfbcb9acfefda39c81b62c06eb56d3f9192a66c
# Parent  6f9111705d4fefa022a319d98fba72c3f49a9e5d
* Pure: improved error reporting of simprocs;
tuned;

diff -r 6f9111705d4f -r 9cfbcb9acfef NEWS
--- 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)
 --------------------------------