[isabelle-dev] Spurious messages

Makarius makarius at sketis.net
Fri Apr 27 23:38:39 CEST 2012

On Fri, 27 Apr 2012, Jasmin Christian Blanchette wrote:

> 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:
>    declare [[unify_search_bound = 55]]
> The declarations are thankfully _not_ ignored.

This is now addressed in Isabelle/53668571d300, using Context_Position 
visiblity to restrict output to messages that are considered relevant to 
the user.


More information about the isabelle-dev mailing list