added some proof state markup, notably number of subgoals (e.g. for indentation);
tuned;

ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;

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