--- 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";