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