*** empty log message ***
authoroheimb
Mon Sep 21 23:16:25 1998 +0200 (1998-09-21)
changeset 552438f2a518a811
parent 5523 dc8cdc192cd0
child 5525 896f8234b864
*** empty log message ***
NEWS
     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