diff -r a3d97348ceb6 -r c82298745c20 NEWS
--- a/NEWS	Thu Oct 10 19:02:23 2002 +0200
+++ b/NEWS	Thu Oct 10 19:03:37 2002 +0200
@@ -74,6 +74,11 @@
 
 *** HOL ***
 
+* new flag trace_unify_fail causes unification to print diagnostic
+information (PG: in trace buffer) when it fails. This is useful for
+figuring out why single step proofs like rule, erule or assumption
+failed.
+
 * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 
 HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";