tuned (all proofs are INSTABLE by David's definition of instability);
authorwenzelm
Wed Oct 21 13:01:17 1998 +0200 (1998-10-21)
changeset 570556f2030c46c6
parent 5704 1ddf7e1e8b19
child 5706 21706a735c8d
tuned (all proofs are INSTABLE by David's definition of instability);
NEWS
     1.1 --- a/NEWS	Wed Oct 21 11:10:38 1998 +0200
     1.2 +++ b/NEWS	Wed Oct 21 13:01:17 1998 +0200
     1.3 @@ -53,10 +53,11 @@
     1.4    delWrapper, delSWrapper: claset *  string            -> claset
     1.5    getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
     1.6  
     1.7 -* Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE semantics;
     1.8 -  addbefore now affects only the unsafe part of step_tac etc.;
     1.9 -  This affects addss/auto_tac/force_tac,so EXISTING (INSTABLE) PROOFS MAY FAIL,
    1.10 -  but proofs should be fixable easily, e.g. by replacing Auto_tac by Force_tac.
    1.11 +* Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE
    1.12 +  semantics; addbefore now affects only the unsafe part of step_tac
    1.13 +  etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
    1.14 +  FAIL, but proofs should be fixable easily, e.g. by replacing
    1.15 +  Auto_tac by Force_tac;
    1.16  
    1.17  * Classical reasoner: setwrapper to setWrapper and compwrapper to compWrapper; 
    1.18    added safe wrapper (and access functions for it);