NEWS
changeset 13644 7e09ff716dc9
parent 13643 c82298745c20
child 13648 610cedff5538
     1.1 --- a/NEWS	Thu Oct 10 19:03:37 2002 +0200
     1.2 +++ b/NEWS	Thu Oct 10 19:24:34 2002 +0200
     1.3 @@ -38,6 +38,11 @@
     1.4  
     1.5    - The simplifier trace now shows the names of the applied rewrite rules
     1.6  
     1.7 +* Pure: new flag trace_unify_fail causes unification to print
     1.8 +diagnostic information (PG: in trace buffer) when it fails. This is
     1.9 +useful for figuring out why single step proofs like rule, erule or
    1.10 +assumption failed.
    1.11 +
    1.12  * Pure: locale specifications now produce predicate definitions
    1.13  according to the body of text (covering assumptions modulo local
    1.14  definitions); predicate "loc_axioms" covers newly introduced text,
    1.15 @@ -74,11 +79,6 @@
    1.16  
    1.17  *** HOL ***
    1.18  
    1.19 -* new flag trace_unify_fail causes unification to print diagnostic
    1.20 -information (PG: in trace buffer) when it fails. This is useful for
    1.21 -figuring out why single step proofs like rule, erule or assumption
    1.22 -failed.
    1.23 -
    1.24  * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 
    1.25  HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
    1.26