tuned

proper context for various Thy_Output options, via official configuration options in ML and Isar;

Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);

eliminated old 'local' command;

more uniform descriptions, which end up in the collective output of 'print_attributes' for example;

Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;

slightly more abstract data handling in Fast_Lin_Arith;

theory data merge: prefer left side uniformly;

tuned;

simplification/standardization of some theory data;

misc tuning and simplification, notably theory data;

renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;

renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;

standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;

merged

merged

consider "locality" when assigning weights to facts

add a bonus for chained facts, since they are likely to be relevant; (especially in a Mirabelle run!) -- chained facts used to be included forcibly, then were treated as any other fact; the current approach seems more flexible

merged

add a penalty for lambda-abstractions; the penalty will kick in only when the goal contains no lambdas, in which case Sledgehammer previously totally disallowed any higher-order construct; this was too drastic; lambdas are dangerous because they rapidly lead to unsound proofs; e.g. COMBI_def COMBS_def not_Cons_self2 with explicit_apply

renaming

fiddle with relevance filter

update docs

reorganize options regarding to the relevance threshold and decay

make relevance filter work in term of a "max_relevant" option + use Vampire SOS; "max_relevant" is more reliable than "max_relevant_per_iter"; also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before; SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)

simplify more code

cosmetics

get rid of "defs_relevant" feature; nobody uses it and it works poorly

make SML/NJ happy

renamed "relevance_convergence" to "relevance_decay"