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

add lemmas lub_APP, lub_LAM

folding on arbitrary Lebesgue integrable functions

fixed spelling errors

move coercions to appropriate places

it is known as the extended reals, not the infinite reals

moved coercion decl. for int

adapting copied bash code in mutabelle script

more correct NEWS;

merged

fix monotonicity type of None

compile

introduced hack to exploit the symmetry of equality in monotonicity calculus

cleanup example

add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule

fixed bug in monotonicity solution display, whereby the polarity of literals was ignored

improve precision of forall in constancy part of the monotonicity calculus

added some missing well-annotatedness constraints to monotonicity calculus

more work on the monotonicity evaluation driver

improve precision of finite functions in monotonicity calculus

added ML code for testing entire theories for monotonicity

use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus

added examples to exercise new monotonicity code

fixed quantifier handling of new monotonicity calculus

tune parentheses and indentation

proper handling of frames for connectives in monotonicity calculus

tune indentation

removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications

implemented All rules from new monotonicity calculus

fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints

started implementing the new monotonicity rules for application

implemented connectives in new monotonicity calculus

added "Neq" operator to monotonicity inference module

started implementing connectives in new monotonicity calculus

more work on frames in the new monotonicity calculus

support 3 monotonicity calculi in one and fix soundness bug

tuning

proper handling of assignment disjunctions vs. conjunctions

adapt monotonicity code to four annotation types

more monotonicity tuning

tuning

added frame component to Gamma in monotonicity calculus

use boolean pair to encode annotation, which may now take four values

started generalizing monotonicity code to accommodate new calculus

merged

handle "max_relevant" uniformly

honor the default max relevant facts setting from the SMT solvers in Sledgehammer

have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?

return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction

trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases

reraise interrupt exceptions

[mq]: sledge_binary_minimizer

correcting usage documentation in mirabelle tool

adding mutabelle as a component and an isabelle tool to be used in regression testing

commenting out sledgehammer_mtd in Mutabelle

removing declaration in quickcheck to really enable exhaustive testing

adding timeout to try invocation in mutabelle

adding filtering, sytactic welltyping, and sledgehammer method in mutabelle

replace `type_mapper` by the more adequate `type_lifting`

moved bootstrap of type_lifting to Fun

replace `type_mapper` by the more adequate `type_lifting`

avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;

IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;

command 'notepad' replaces former 'example_proof';

prefer 'notepad' over 'example_proof';

merged

more intimate definition of fold_list / fold_once in terms of fold

canonical fold signature

formal notepad without any result;

added Syntax.default_root; simplified Syntax.parse operations; clarified treatment of syntax root for translation rules -- refrain from logical_type replacement; tuned error message;

eliminated obsolete Token.Malformed -- subsumed by Token.Error;

tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);

added Syntax.pretty_priority;

merged

conventional point-free characterization of rsp_fold

replaced memb by existing List.member

explicit type constraint; streamlined notation

tuned proposition

lemma multiset_of_rev

lemmas fold_remove1_split and fold_multiset_equiv

minor tuning for release;

source files are always encoded as UTF-8;

eliminated fragile HTML.with_charset -- always use utf-8;

recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;

removed old generated stuff; removed DOS line endings;

comment;

update documentation

replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us

export more information about available SMT solvers