HOL/Import: Fix errors with _mk_list

Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);

simplified malformed YXML markup -- special controls are visible in IsabelleText font;

less ambitious ProofGeneral markup, which occasionally breaks plain-old regexps in elisp;

more robust Binding.pretty/print in typical error sitations with spaces etc. (NB: markup can only provide *additional* emphasis and is occasionally suppressed in TTY mode or tooltips);

more visible printing of empty binding;

do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;

more quotes;

merged

added missing dependencies; simplified (by overapproximating a bit); alphabetical order

merged

merged

tuned notation and proofs

move error logic closer to user

allow lambda-lifting without triggers

move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)

added option to control which lambda translation to use (for experiments)

fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem

use monomorphic encoding as fallback, since they tend to produce fewer type errors

don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes

clearer unsound message

clarify fine soundness point

always unfold "Let"s is Sledgehammer, Metis, and MESON

unbreak Nitrox's parsing

merged

tuned lemma positions and proofs

tuned notation

uniqueness lemmas for bot and top

adjusted to tightened specification of classes bot and top

moved lemmas bot_less and less_top to classes bot and top respectively