# HG changeset patch
# User oheimb
# Date 906412585 -7200
# Node ID 38f2a518a811cc8267a355530236c903d78898a0
# Parent  dc8cdc192cd019a57d3d7910808093a405e11099
*** empty log message ***

diff -r dc8cdc192cd0 -r 38f2a518a811 NEWS
--- a/NEWS	Mon Sep 21 23:14:33 1998 +0200
+++ b/NEWS	Mon Sep 21 23:16:25 1998 +0200
@@ -47,6 +47,14 @@
   delWrapper, delSWrapper: claset *  string            -> claset
   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
 
+* Classical reasoner: addbefore / addSbefore now have APPEND / ORELSE semantics;
+  addbefore now affects only the unsafe part of step_tac etc.;
+  This affects addss/auto_tac/force_tac, so EXISTING (INSTABLE) PROOFS MAY FAIL, but
+  most proofs should be fixable easily, e.g. by replacing Auto_tac by Force_tac.
+
+* Classical reasoner: setwrapper to setWrapper and compwrapper to compWrapper; 
+  added safe wrapper (and access functions for it);
+
 * HOL/split_all_tac is now much faster and fails if there is nothing
 to split.  Existing (fragile) proofs may require adaption because the
 order and the names of the automatically generated variables have