# HG changeset patch
# User oheimb
# Date 856194659 -3600
# Node ID 2edc5b01e5a77e894ffb550cb4ebfd2d9996adb7
# Parent  9944bea3b459787a9e9ed27154aa00eb4c3df151
improved description of recent changes

diff -r 9944bea3b459 -r 2edc5b01e5a7 NEWS
--- a/NEWS	Mon Feb 17 16:50:17 1997 +0100
+++ b/NEWS	Mon Feb 17 16:50:59 1997 +0100
@@ -2,6 +2,9 @@
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
+New in Isabelle94-8 (??????????? 1997 FIXME)
+---------------------------------------
+
 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
 
 * simplifier: the solver is now split into a safe and an unsafe part.
@@ -9,21 +12,16 @@
   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,
+* classical reasoner: little changes in semantics of addafter (now: addaltern),
+  renamed setwrapper to setWrapper, addwrapper to addWrapper
   added safe wrapper (and access functions for it)
 
-* better combination of classical reasoner and simplifier: 
+* improved 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)
----------------------------------------
+  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
 
 * HOL: primrec now also works with type nat;