--- a/NEWS Sat Feb 15 17:55:11 1997 +0100
+++ b/NEWS Sat Feb 15 18:24:05 1997 +0100
@@ -2,6 +2,25 @@
Isabelle NEWS -- history of user-visible changes
================================================
+* simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
+
+* simplifier: the solver is now split into a safe and an unsafe part.
+ This should be invisible for the normal user, except that the functions
+ setsolver and addsolver have been renamed to setSolver and addSolver.
+ added safe_asm_full_simp_tac.
+
+* classical reasoner: better addbefore, addafter (now: addaltern),
+ setwrapper (now: setWrapper) and addwrapper (now addWrapper)
+ replaced addafter by addaltern,
+ added safe wrapper (and access functions for it)
+
+* better combination of classical reasoner and simplifier:
+ new addss, auto_tac, functions for handling clasimpsets, ...
+ Now, the simplification is safe (therefore moved to safe_step_tac) and thus
+ more complete, as multiple instantiation of unknowns (with slow_tac)possible
+ COULD MAKE EXISTING PROOFS FAIL; in case of problems with unstable
+ old proofs, use unsafe_addss and unsafe_auto_tac
+
New in Isabelle94-8 (??????????? 1997 FIXME)
---------------------------------------