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

tuned instantiations dropped redundant lemmas

unify Card_Univ and Cardinality

definition less_int_def has changed, use 'less_le' instead

adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets