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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
