don't use aggressive with HO ATP

more aggressive type argument optimization

use cover for "poly_guards" encoding

hack to make LEO-II perform better on TPTP THF problems

swap adjectives (cf. Google)

tweaked remote Vampire version

don't cripple Sledgehammer/ATP needlessly just because of "metis" -- there's also "smt" as a fallback anyway

apply preprocessing simpset also to rhs of abstract code equations

clarified code translation code

prefer sys.error over plain error in Scala to avoid deprecation warning

prefer records with speaking labels over deeply nested tuples

merged

more sort constraints for FinFun code generation

restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"

explicit check for correct number of arguments for abstract constructor

merged

transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters

transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules

unify theory-data structures for transfer package

remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit

improved code setup for card, finite, subset

merged

more instantiations for card_UNIV, more lemmas for CARD

simplify card_UNIV type class, tuned proofs

drop redundant sort constraint

use \tocentry as in implementation manual;

tuned message;

tuned header;

merged

tuned proofs