improved description of recent changes
authoroheimb
Mon Feb 17 16:50:59 1997 +0100 (1997-02-17)
changeset 26492edc5b01e5a7
parent 2648 9944bea3b459
child 2650 96234bf96bf9
improved description of recent changes
NEWS
     1.1 --- a/NEWS	Mon Feb 17 16:50:17 1997 +0100
     1.2 +++ b/NEWS	Mon Feb 17 16:50:59 1997 +0100
     1.3 @@ -2,6 +2,9 @@
     1.4  Isabelle NEWS -- history of user-visible changes
     1.5  ================================================
     1.6  
     1.7 +New in Isabelle94-8 (??????????? 1997 FIXME)
     1.8 +---------------------------------------
     1.9 +
    1.10  * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
    1.11  
    1.12  * simplifier: the solver is now split into a safe and an unsafe part.
    1.13 @@ -9,21 +12,16 @@
    1.14    setsolver and addsolver have been renamed to setSolver and addSolver.
    1.15    added safe_asm_full_simp_tac. 
    1.16  
    1.17 -* classical reasoner: better addbefore, addafter (now: addaltern),
    1.18 -	setwrapper (now: setWrapper) and addwrapper (now addWrapper)
    1.19 -  replaced addafter by addaltern,
    1.20 +* classical reasoner: little changes in semantics of addafter (now: addaltern),
    1.21 +  renamed setwrapper to setWrapper, addwrapper to addWrapper
    1.22    added safe wrapper (and access functions for it)
    1.23  
    1.24 -* better combination of classical reasoner and simplifier: 
    1.25 +* improved combination of classical reasoner and simplifier: 
    1.26    new addss, auto_tac, functions for handling clasimpsets, ...
    1.27    Now, the simplification is safe (therefore moved to safe_step_tac) and thus
    1.28 -  more complete, as multiple instantiation of unknowns (with slow_tac)possible
    1.29 -  COULD MAKE EXISTING PROOFS FAIL; in case of problems with unstable 
    1.30 -  old proofs, use unsafe_addss and unsafe_auto_tac
    1.31 -
    1.32 -
    1.33 -New in Isabelle94-8 (??????????? 1997 FIXME)
    1.34 ----------------------------------------
    1.35 +  more complete, as multiple instantiation of unknowns (with slow_tac) possible
    1.36 +  COULD MAKE EXISTING PROOFS FAIL; in case of problems with unstable old proofs:
    1.37 +                                   use unsafe_addss and unsafe_auto_tac
    1.38  
    1.39  * HOL: primrec now also works with type nat;
    1.40