Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 2014-RC1 issues: unify_trace_failure

Email Gateway (Aug 19 2022 at 15:43):

From: Lars Noschinski <noschinl@in.tum.de>
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

Email Gateway (Aug 19 2022 at 15:44):

From: Makarius <makarius@sketis.net>
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.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC