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

name filter operation just filter (c.f. List.filter and list comprehension syntax)

tuned whitespace

eliminated some hard tabulators (deprecated);

pass constant arguments to the built-in check function, cf. d2b1fc1b8e19

merged

updated SMT certificates

reduced unnecessary complexity; improved documentation; tuned

tuned

centralized handling of built-in types and constants for bitvectors

moved smt_word.ML into the directory of the Word library

centralized handling of built-in types and constants; also store types and constants which are rewritten during preprocessing; interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols); removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)

more aggressive unfolding of unknowns in Z3 models

tuned

adding a definition for refl_on which is friendly for quickcheck and nitpick

merged

simplify monotonicity code after killing "fin_fun" optimization

updated Nitpick's documentation w.r.t. finitization

remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much

give the inner timeout mechanism a chance, since it gives more precise information to the user

updated monotonicity calculus w.r.t. set products

removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil

added a hint when the user obviously just forgot a colon after the lemma's name

simplified special handling of set products

fix special handling of set products

use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets

merged

testing smartly in two dimensions (cardinality and size) in quickcheck

load "try" after "Metis" and move "Async_Manager" back to Sledgehammer

make SML/NJ happy

merge

show strings as "s_1" etc. rather than "l_1" etc.

quiet Metis in "try"

removed experimental equality checking of closures; acknowledge underapproximation of equality in function name

add set-union-like syntax for powerdomain bind operators

merged

instance unit :: domain

simplify ideal completion proofs

remove unused lemmas

remove lemma cont_cfun; rename thelub_cfun to lub_cfun

rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun

pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead

cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo