NEWS
changeset 5524 38f2a518a811
parent 5490 85855f65d0c6
child 5526 e7617b57a3e6
     1.1 --- a/NEWS	Mon Sep 21 23:14:33 1998 +0200
     1.2 +++ b/NEWS	Mon Sep 21 23:16:25 1998 +0200
     1.3 @@ -47,6 +47,14 @@
     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, but
    1.10 +  most proofs should be fixable easily, e.g. by replacing Auto_tac by Force_tac.
    1.11 +
    1.12 +* Classical reasoner: setwrapper to setWrapper and compwrapper to compWrapper; 
    1.13 +  added safe wrapper (and access functions for it);
    1.14 +
    1.15  * HOL/split_all_tac is now much faster and fails if there is nothing
    1.16  to split.  Existing (fragile) proofs may require adaption because the
    1.17  order and the names of the automatically generated variables have