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