[isabelle-dev] trace_unify_fail

Lars Noschinski noschinl at in.tum.de
Fri Sep 13 18:36:09 CEST 2013


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

More information about the isabelle-dev mailing list