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;
2011-03-20 wenzelm 2011-03-20 pervasive cond_timeit;
2011-03-20 wenzelm 2011-03-20 eliminated dead code;
2011-03-20 wenzelm 2011-03-20 parallel preparation of document variants, within separate directories;
2011-03-20 wenzelm 2011-03-20 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections; tuned;
2011-03-20 wenzelm 2011-03-20 eliminated redundant doc_prefix1; tuned;
2011-03-20 wenzelm 2011-03-20 renamed doc_prefix2 to dump_prefix;
2011-03-20 wenzelm 2011-03-20 tuned;
2011-03-20 wenzelm 2011-03-20 tuned terminology for document variants;
2011-03-20 wenzelm 2011-03-20 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;
2011-03-20 wenzelm 2011-03-20 tuned;
2011-03-19 blanchet 2011-03-19 preencode value of "need" selectors in Kodkod bounds as an optimization
2011-03-19 blanchet 2011-03-19 ignore "need" axioms for "nat"-like types