*** empty log message ***
authoroheimb
Sat Feb 15 18:24:05 1997 +0100 (1997-02-15)
changeset 26392c38796b33b9
parent 2638 6c6a44b5f757
child 2640 ee4dfce170a0
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Sat Feb 15 17:55:11 1997 +0100
     1.2 +++ b/NEWS	Sat Feb 15 18:24:05 1997 +0100
     1.3 @@ -2,6 +2,25 @@
     1.4  Isabelle NEWS -- history of user-visible changes
     1.5  ================================================
     1.6  
     1.7 +* simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
     1.8 +
     1.9 +* simplifier: the solver is now split into a safe and an unsafe part.
    1.10 +  This should be invisible for the normal user, except that the functions
    1.11 +  setsolver and addsolver have been renamed to setSolver and addSolver.
    1.12 +  added safe_asm_full_simp_tac. 
    1.13 +
    1.14 +* classical reasoner: better addbefore, addafter (now: addaltern),
    1.15 +	setwrapper (now: setWrapper) and addwrapper (now addWrapper)
    1.16 +  replaced addafter by addaltern,
    1.17 +  added safe wrapper (and access functions for it)
    1.18 +
    1.19 +* better combination of classical reasoner and simplifier: 
    1.20 +  new addss, auto_tac, functions for handling clasimpsets, ...
    1.21 +  Now, the simplification is safe (therefore moved to safe_step_tac) and thus
    1.22 +  more complete, as multiple instantiation of unknowns (with slow_tac)possible
    1.23 +  COULD MAKE EXISTING PROOFS FAIL; in case of problems with unstable 
    1.24 +  old proofs, use unsafe_addss and unsafe_auto_tac
    1.25 +
    1.26  
    1.27  New in Isabelle94-8 (??????????? 1997 FIXME)
    1.28  ---------------------------------------