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