NEWS
changeset 13643 c82298745c20
parent 13618 12290bdce807
child 13644 7e09ff716dc9
     1.1 --- a/NEWS	Thu Oct 10 19:02:23 2002 +0200
     1.2 +++ b/NEWS	Thu Oct 10 19:03:37 2002 +0200
     1.3 @@ -74,6 +74,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* new flag trace_unify_fail causes unification to print diagnostic
     1.8 +information (PG: in trace buffer) when it fails. This is useful for
     1.9 +figuring out why single step proofs like rule, erule or assumption
    1.10 +failed.
    1.11 +
    1.12  * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 
    1.13  HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
    1.14