move facts supplied with "add:" to the front, so that they get a better weight (SMT)

beautify MacLaurin proofs; make better use of DERIV_intros

workaround for bug in weight handling -- sometimes numerals got replaced by Vars and this confused the weight extractor

avoid ML structure aliases (especially single-letter abbreviations);

eliminated dead code;

more correct ML snippets that are unchecked; tuned comments;

merged

Added two theorems about the concept of range. Tidied up the comments.

honor "overlord" option for SMT solvers as well and don't pass "ext" to them

make Sledgehammer's relevance filter include the "ext" rule when appropriate

tuning

tuning

added support for "type_sys" option to Mirabelle

honor "metisFT" in Mirabelle

make "full_types" take precedence over "type_sys"

crank up Metis's timeout for SMT solvers, since users love Metis

generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction

make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences

consider "finite" overloaded in "precise_overloaded_args" mode

added timeout max for remote server invocation

fix translation of higher-order equality ("fequal") if "precise_overloaded_args" is "true"

fix Vampire parsing problem

improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags

example tuning

remove at most one double negation -- any other double negations are part of some higher-order reasoning and should be left alone, cf. "HO_Reas.thy"

weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed

added example to exercise higher-order reasoning with Sledgehammer and Metis

added Sledgehammer support for higher-order propositional reasoning

add Metis support for higher-order propositional reasoning

implemented partially-typed "tags" type encoding