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
begin
declare [[unify_search_bound = 55]]
declare [[unify_trace_bound = 55]]
The declarations are thankfully _not_ ignored.
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
