# HG changeset patch
# User oheimb
# Date 856027445 -3600
# Node ID 2c38796b33b9e2cabd5328cc2d23d994211ba32c
# Parent  6c6a44b5f7576fffda0b28c6ecafec50e24922db
*** empty log message ***

diff -r 6c6a44b5f757 -r 2c38796b33b9 NEWS
--- 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)
 ---------------------------------------