Re: [isabelle] 2014-RC1 issues: unify_trace_failure



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

declare [[unify_trace_failure]]

end




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.