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

definition less_int_def has changed, use 'less_le' instead

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

remove stray reference to no-longer-existing theorem 'add'

temporarily comment out portion of Quotient_Examples/Quotient_Rat.thy, broken by changes to Int.thy

temporarily comment out nitpick examples broken by changes to Int.thy

convert Int.thy to use lifting and transfer

remove unnecessary simp rules involving Abs_Integ

introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)

merged

remove pretty syntax for FinFuns at the end and provide separate syntax theory

add lemma set_of_image_mset

merged

eliminated remaining sub- and superscripts in FinFun syntax

syntax for FinFun composition without subscripts tuned proofs

FinFun pseudo-constructor syntax without superscripts

replace FinFun application syntax with $

removed subscripts from FinFun type syntax

improve code setup for set equality

add code equation for coset xs = set ys

tuned proofs

use bundle in FinFun

unify Rep_finfun and finfun_apply

move FinFuns from AFP to repository

discontinued unused unzip/untar;

update GUI components after init;

merged

don't be so aggressive during unfolding id and o

reordered sections

tuned message;