merged

Integrated set comprehension pointfree simproc.

Improved tactic for rewriting set comprehensions into pointfree form. Currently the simproc targets a term with an arbitrary number of conjuncts of form "x : S". The tactic should now handle all cases of this form.

Updated comment to reflect current state.

clarifying comment

sound monotonicity inference in the presence of "aggressive" helpers

less confusing error message

removed dead code

class target handles additional non-class term parameters appropriately

merged

add lemma to FinFun

fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users

tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings

pass more facts to LEO-II, in the light of latest evaluation

prevent an "Empty" exception (e.g. with Satallax, "mono_native")

tuning terminology

updated NEWS

updated docs

added "args_query" encodings

removed killed encodings from Metis examples

updated docs

killed most unsound encodings

generalized monotonic constructor optimisation so that it works with e.g. the product type

removed micro-optimization whose justification I can't recall

add missing timeout multiplier

avoid dumping definitions several times in LEO-II proofs

robust LEO-II setup that doesn't rely on ".leoatprc"

renamed TPTP commands to agree with Sutcliffe's terminology

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

tuned instantiations dropped redundant lemmas

unify Card_Univ and Cardinality