[isabelle-dev] trace_unify_fail

[Lars Noschinski]

Hi,

I just spent some time discovering where trace_unify_fail went (there 
now exists an attribute unify_trace_failure). As the introduction of 
this flag had a NEWS entry, wouldn't this change also merit a NEWS entry 
(in particular, as it is not documented in the reference manual)?

Even if it is crude to use (due to it being a global-only option), it is 
an important debugging tool, in particular with large goals as you get 
in program verification.

   -- Lars