Mercurialisabelle / shortlog
summary | shortlog | changelog | graph | tags | branches | files | gz

 
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 changeset | files
2011-03-23 boehmes 2011-03-23 really be quiet changeset | files
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 changeset | files
2011-03-22 wenzelm 2011-03-22 merged changeset | files
2011-03-22 hoelzl 2011-03-22 standardized headers changeset | files
2011-03-22 hoelzl 2011-03-22 generalized Caratheodory from algebra to ring_of_sets changeset | files
2011-03-22 hoelzl 2011-03-22 add ring_of_sets and subset_class as basis for algebra changeset | files
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 changeset | files
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 changeset | files
2011-03-22 blanchet 2011-03-22 remove lie from documentation changeset | files
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 changeset | files
2011-03-22 blanchet 2011-03-22 make Minimizer honor "verbose" and "debug" options better changeset | files
2011-03-22 nipkow 2011-03-22 fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples changeset | files
2011-03-21 krauss 2011-03-21 moved some configurations to AFP, and fixed others changeset | files
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; changeset | files
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; changeset | files
2011-03-22 wenzelm 2011-03-22 binder_tr: more informative exception; changeset | files
2011-03-22 wenzelm 2011-03-22 Hoare syntax: strip positions where they crash translation functions; re-unified some clones (!); changeset | files
2011-03-22 wenzelm 2011-03-22 update_name_tr: more precise handling of explicit constraints, including positions; changeset | files
2011-03-22 wenzelm 2011-03-22 statespace syntax: strip positions -- type constraints are unexpected here; changeset | files
2011-03-22 wenzelm 2011-03-22 let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information); changeset | files
2011-03-22 wenzelm 2011-03-22 datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn"; changeset | files
2011-03-22 wenzelm 2011-03-22 tuned indendation and parentheses; changeset | files
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; changeset | files
2011-03-22 wenzelm 2011-03-22 pretty_string: proper handling of negative max_len; changeset | files
2011-03-21 wenzelm 2011-03-21 added Lexicon.encode_position, Lexicon.decode_position; changeset | files
2011-03-21 wenzelm 2011-03-21 tuned; changeset | files
2011-03-21 wenzelm 2011-03-21 tuned; changeset | files
2011-03-21 wenzelm 2011-03-21 clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term; changeset | files
2011-03-21 wenzelm 2011-03-21 tuned; changeset | files
2011-03-21 wenzelm 2011-03-21 merged changeset | files
2011-03-21 krauss 2011-03-21 added judgement day configurations changeset | files
2011-03-21 wenzelm 2011-03-21 another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc); changeset | files
2011-03-21 krauss 2011-03-21 fixed perl error changeset | files
2011-03-21 krauss 2011-03-21 eliminated unnecessary generated ROOT.ML changeset | files
2011-03-21 krauss 2011-03-21 more precise dependencies changeset | files
2011-03-21 krauss 2011-03-21 small test case for main mirabelle functionality, which easily breaks without noticing changeset | files
2011-03-21 krauss 2011-03-21 propagate mirabelle failures properly; flatten obscure return code semantics of Perl system command to 0/1 changeset | files
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) changeset | files
2011-03-21 bulwahn 2011-03-21 merged changeset | files
2011-03-18 bulwahn 2011-03-18 adapting predicate_compile_quickcheck; tuned changeset | files
2011-03-18 bulwahn 2011-03-18 adapting mutabelle changeset | files
2011-03-18 bulwahn 2011-03-18 adapting SML_Quickcheck changeset | files
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 changeset | files
2011-03-18 bulwahn 2011-03-18 extending the test data generators to take the evaluation terms as arguments changeset | files
2011-03-18 bulwahn 2011-03-18 adding option of evaluating terms after invocation in quickcheck changeset | files
2011-03-18 bulwahn 2011-03-18 adding eval option to quickcheck changeset | files
2011-03-18 bulwahn 2011-03-18 handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation changeset | files
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 changeset | files
2011-03-18 bulwahn 2011-03-18 adding a simple datatype for representing functions in Quickcheck_Narrowing changeset | files
2011-03-18 bulwahn 2011-03-18 extending code_int type more; adding narrowing instance for type int; added test case for int instance changeset | files
2011-03-18 bulwahn 2011-03-18 translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases changeset | files
2011-03-18 bulwahn 2011-03-18 adding size as static argument in quickcheck_narrowing compilation changeset | files
2011-03-20 wenzelm 2011-03-20 modernized specifications; changeset | files
2011-03-20 wenzelm 2011-03-20 dropped unused structure aliases; changeset | files
2011-03-20 wenzelm 2011-03-20 tuned; changeset | files
2011-03-20 wenzelm 2011-03-20 NEWS: structure Timing provides various operations for timing; changeset | files
2011-03-20 wenzelm 2011-03-20 simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing); changeset | files
2011-03-20 wenzelm 2011-03-20 pure Timing.timing, without any exception handling; clarified cond_timeit: propagate interrupt without side-effect; changeset | files
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; changeset | files
isabelle