2011-03-23 blanchet 2011-03-23 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" default to "e" rather than "vampire" since E is part of the Isabelle bundle
2011-03-23 boehmes 2011-03-23 really be quiet
2011-03-23 krauss 2011-03-23 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
2011-03-22 wenzelm 2011-03-22 merged
2011-03-22 hoelzl 2011-03-22 standardized headers
2011-03-22 hoelzl 2011-03-22 generalized Caratheodory from algebra to ring_of_sets
2011-03-22 hoelzl 2011-03-22 add ring_of_sets and subset_class as basis for algebra
2011-03-22 blanchet 2011-03-22 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
2011-03-22 blanchet 2011-03-22 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
2011-03-22 blanchet 2011-03-22 remove lie from documentation
2011-03-22 blanchet 2011-03-22 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
2011-03-22 blanchet 2011-03-22 make Minimizer honor "verbose" and "debug" options better
2011-03-22 nipkow 2011-03-22 fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
2011-03-21 krauss 2011-03-21 moved some configurations to AFP, and fixed others
2011-03-22 wenzelm 2011-03-22 more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-03-22 wenzelm 2011-03-22 enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;
2011-03-22 wenzelm 2011-03-22 binder_tr: more informative exception;
2011-03-22 wenzelm 2011-03-22 Hoare syntax: strip positions where they crash translation functions; re-unified some clones (!);
2011-03-22 wenzelm 2011-03-22 update_name_tr: more precise handling of explicit constraints, including positions;
2011-03-22 wenzelm 2011-03-22 statespace syntax: strip positions -- type constraints are unexpected here;
2011-03-22 wenzelm 2011-03-22 let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
2011-03-22 wenzelm 2011-03-22 datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
2011-03-22 wenzelm 2011-03-22 tuned indendation and parentheses;
2011-03-22 wenzelm 2011-03-22 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;
2011-03-22 wenzelm 2011-03-22 pretty_string: proper handling of negative max_len;
2011-03-21 wenzelm 2011-03-21 added Lexicon.encode_position, Lexicon.decode_position;
2011-03-21 wenzelm 2011-03-21 tuned;
2011-03-21 wenzelm 2011-03-21 tuned;
2011-03-21 wenzelm 2011-03-21 clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
2011-03-21 wenzelm 2011-03-21 tuned;
2011-03-21 wenzelm 2011-03-21 merged
2011-03-21 krauss 2011-03-21 added judgement day configurations
2011-03-21 wenzelm 2011-03-21 another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
2011-03-21 krauss 2011-03-21 fixed perl error
2011-03-21 krauss 2011-03-21 eliminated unnecessary generated ROOT.ML
2011-03-21 krauss 2011-03-21 more precise dependencies
2011-03-21 krauss 2011-03-21 small test case for main mirabelle functionality, which easily breaks without noticing
2011-03-21 krauss 2011-03-21 propagate mirabelle failures properly; flatten obscure return code semantics of Perl system command to 0/1
2011-03-21 krauss 2011-03-21 mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
2011-03-21 bulwahn 2011-03-21 merged
2011-03-18 bulwahn 2011-03-18 adapting predicate_compile_quickcheck; tuned
2011-03-18 bulwahn 2011-03-18 adapting mutabelle
2011-03-18 bulwahn 2011-03-18 adapting SML_Quickcheck
2011-03-18 bulwahn 2011-03-18 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
2011-03-18 bulwahn 2011-03-18 extending the test data generators to take the evaluation terms as arguments
2011-03-18 bulwahn 2011-03-18 adding option of evaluating terms after invocation in quickcheck
2011-03-18 bulwahn 2011-03-18 adding eval option to quickcheck
2011-03-18 bulwahn 2011-03-18 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
2011-03-18 bulwahn 2011-03-18 adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
2011-03-18 bulwahn 2011-03-18 adding a simple datatype for representing functions in Quickcheck_Narrowing
2011-03-18 bulwahn 2011-03-18 extending code_int type more; adding narrowing instance for type int; added test case for int instance
2011-03-18 bulwahn 2011-03-18 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
2011-03-18 bulwahn 2011-03-18 adding size as static argument in quickcheck_narrowing compilation
2011-03-20 wenzelm 2011-03-20 modernized specifications;
2011-03-20 wenzelm 2011-03-20 dropped unused structure aliases;
2011-03-20 wenzelm 2011-03-20 tuned;
2011-03-20 wenzelm 2011-03-20 NEWS: structure Timing provides various operations for timing;
2011-03-20 wenzelm 2011-03-20 simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
2011-03-20 wenzelm 2011-03-20 pure Timing.timing, without any exception handling; clarified cond_timeit: propagate interrupt without side-effect;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;