added "SMT." qualifier for constant to make it possible to reload "smt_monomorph.ML" from outside the "SMT" theory (for experiments) -- this is also consistent with the other SMT constants mentioned in this source file

reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions

unfold set constants in Sledgehammer/ATP as well if Metis does it too

do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings

renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly

added unfold set constant functionality to Meson/Metis -- disabled by default for now

remove unused parameter

reduced penalty associated with existential quantifiers

ensure that Auto Sledgehammer is run with full type information

fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized

don't give weights to built-in symbols

more robust exception handling in Metis (also works if there are several subgoals)

no penality for constants that appear in chained facts

gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers