tuned (all proofs are INSTABLE by David's definition of instability);
authorwenzelm
Wed, 21 Oct 1998 13:01:17 +0200
changeset 5705 56f2030c46c6
parent 5704 1ddf7e1e8b19
child 5706 21706a735c8d
tuned (all proofs are INSTABLE by David's definition of instability);
NEWS
--- a/NEWS	Wed Oct 21 11:10:38 1998 +0200
+++ b/NEWS	Wed Oct 21 13:01:17 1998 +0200
@@ -53,10 +53,11 @@
   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 proofs should be fixable easily, e.g. by replacing Auto_tac by Force_tac.
+* 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 PROOFS MAY
+  FAIL, but 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);