| changeset 13643 | c82298745c20 |
| parent 13618 | 12290bdce807 |
| child 13644 | 7e09ff716dc9 |
--- a/NEWS Thu Oct 10 19:02:23 2002 +0200 +++ b/NEWS Thu Oct 10 19:03:37 2002 +0200 @@ -74,6 +74,11 @@ *** 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";