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.
More information about the isabelle-dev