pretty_string: proper handling of negative max_len;

added Lexicon.encode_position, Lexicon.decode_position;

tuned;

tuned;

clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;

tuned;

merged

added judgement day configurations

another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);

fixed perl error

eliminated unnecessary generated ROOT.ML

more precise dependencies

small test case for main mirabelle functionality, which easily breaks without noticing

propagate mirabelle failures properly; flatten obscure return code semantics of Perl system command to 0/1

mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)

merged

adapting predicate_compile_quickcheck; tuned

adapting mutabelle

adapting SML_Quickcheck

passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing

extending the test data generators to take the evaluation terms as arguments

adding option of evaluating terms after invocation in quickcheck

adding eval option to quickcheck

handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation

adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing

adding a simple datatype for representing functions in Quickcheck_Narrowing

extending code_int type more; adding narrowing instance for type int; added test case for int instance

translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases

adding size as static argument in quickcheck_narrowing compilation

modernized specifications;

dropped unused structure aliases;

tuned;

NEWS: structure Timing provides various operations for timing;

simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);

pure Timing.timing, without any exception handling; clarified cond_timeit: propagate interrupt without side-effect;

structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;

pervasive cond_timeit;

eliminated dead code;

parallel preparation of document variants, within separate directories;

Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections; tuned;

eliminated redundant doc_prefix1; tuned;

renamed doc_prefix2 to dump_prefix;

tuned;

tuned terminology for document variants;

replaced File.check by specific File.check_file, File.check_dir; clarified File.full_path -- include parts of former Thy_Load.get_file; simplified Thy_Load.check_file -- do not read/digest yet; merged Thy_Load.check_thy/deps_thy -- always read text and parse header; clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator; Thy_Info.check_deps etc.: File.read exactly once;

tuned;

preencode value of "need" selectors in Kodkod bounds as an optimization

ignore "need" axioms for "nat"-like types

added "simp:", "intro:", and "elim:" to "try" command

optimize Kodkod axioms further w.r.t. "need" option

optimize Kodkod bounds of nat-like datatypes

more optimizations of bounds for "need"

optimize Kodkod bounds when "need" is specified

always destroy constructor patterns, since this seems to be always useful

reintroduced "show_skolems" option -- useful when too many Skolems are displayed

reword Nitpick's wording concerning potential counterexamples

prevent an exception if "card" is empty (e.g., "nitpick [card]")

add option to function to keep trivial ATP formulas, needed for some experiments

add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)

tuned lemma