[isabelle-dev] Spurious messages

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri Apr 27 14:25:31 CEST 2012

Hi all,

With the latest Isabelle (44b33c1e702e), some attributes, e.g. "unify_search" bound, give pairs of spurious warnings, e.g.

    ### Ignoring local change of global option "unify_search_bound"

even when they are declared globally, as in the theory below:

    theory Scratch
    imports Main

    declare [[unify_search_bound = 55]]
    declare [[unify_trace_bound = 55]]

The declarations are thankfully _not_ ignored.


More information about the isabelle-dev mailing list