*** empty log message ***
authornipkow
Thu Oct 10 19:03:37 2002 +0200 (2002-10-10)
changeset 13643c82298745c20
parent 13642 a3d97348ceb6
child 13644 7e09ff716dc9
*** empty log message ***
NEWS
     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