tracing of term to be evaluated

merged

use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand

integral over setprod

cleanup bijectivity btw. product spaces and pairs

compile

lower fudge factor

reword error message

implicitly call the minimizer for SMT solvers that don't return an unsat core

renamings

moved function to later module

clarified terminology

split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems

if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck

adding a smarter enumeration scheme for finite functions

merged

work around problems with eta-expansion of equations

bot comes before top, inf before sup etc.

tuned

nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules

NEWS

adding more efficient implementations for quantifiers in Enum

improving the mutabelle script

primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`; tuned

primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`

hide popular names R and B

built-in numbers are also built-in terms

be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)

merged

more concise case names; proved extensionality