NEWS
changeset 13644 7e09ff716dc9
parent 13643 c82298745c20
child 13648 610cedff5538
--- a/NEWS	Thu Oct 10 19:03:37 2002 +0200
+++ b/NEWS	Thu Oct 10 19:24:34 2002 +0200
@@ -38,6 +38,11 @@
 
   - The simplifier trace now shows the names of the applied rewrite rules
 
+* Pure: 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.
+
 * Pure: locale specifications now produce predicate definitions
 according to the body of text (covering assumptions modulo local
 definitions); predicate "loc_axioms" covers newly introduced text,
@@ -74,11 +79,6 @@
 
 *** 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";