Re: [isabelle] 2014-RC1 issues: unify_trace_failure
On Mon, 4 Aug 2014, Lars Noschinski wrote:
Even when declared inside a global context, the attribute
unify_trace_failure emits the warning
Ignoring local change of global option "unify_trace_failure"
two times. Reproduce with:
theory Scratch imports Pure begin
Thanks for looking after such details. I have made 2-3 rounds over
critical spots where warnings get emitted, and reduced the redundancy for
the next release candidate.
This archive was generated by a fusion of
Pipermail (Mailman edition) and