replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH

merged

standardized headers

generalized Caratheodory from algebra to ring_of_sets

add ring_of_sets and subset_class as basis for algebra

added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter

added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers

remove lie from documentation

let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now

make Minimizer honor "verbose" and "debug" options better

fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples

moved some configurations to AFP, and fixed others

more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;

enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;

binder_tr: more informative exception;

Hoare syntax: strip positions where they crash translation functions; re-unified some clones (!);

update_name_tr: more precise handling of explicit constraints, including positions;

statespace syntax: strip positions -- type constraints are unexpected here;

let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);

datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";

tuned indendation and parentheses;

support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;

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;