2010-12-03 bulwahn 2010-12-03 moving iteration of tests to the testers in quickcheck
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-09 bulwahn 2010-09-09 removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
2010-09-09 bulwahn 2010-09-09 changing the container for the quickcheck options to a generic data
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-11 wenzelm 2010-08-11 use Pretty.enum convenience;
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-24 wenzelm 2010-06-24 avoid equality on abstract type Pretty.T;
2010-06-10 haftmann 2010-06-10 moved inductive_codegen to place where product type is available; tuned structure name
2010-05-30 wenzelm 2010-05-30 replaced ML_Lex.read_antiq by more concise, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-28 wenzelm 2010-03-28 static defaults for configuration options;
2010-03-28 wenzelm 2010-03-28 use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
2010-02-26 bulwahn 2010-02-26 merged
2010-02-25 bulwahn 2010-02-25 added basic reporting of test cases to quickcheck
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-22 haftmann 2010-01-22 HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2009-11-27 haftmann 2009-11-27 renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
2009-11-19 berghofe 2009-11-19 Added new counterexample generator SML_inductive for goals involving inductive predicates.
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 Datatype.read_typ: standard argument order; eliminated some old folds;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-07-30 haftmann 2009-07-30 path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
2009-07-29 haftmann 2009-07-29 cleaned up abstract tuple operations and named them consistently
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-29 haftmann 2009-06-29 explicit Set constructor for code generated for sets
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-01 wenzelm 2009-01-01 eliminated OldTerm.(add_)term_consts;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-10-09 haftmann 2008-10-09 established canonical argument order in SML code generators
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-30 haftmann 2008-06-30 simplified retrieval of theory names of consts and types
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2007-09-18 haftmann 2007-09-18 separated code for inductive sequences from inductive_codegen.ML
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-28 berghofe 2007-08-28 Added sequences with recursion depth limit.
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-08-02 berghofe 2007-08-02 - Added cycle test to function mk_ind_def to avoid non-termination of code generator. - Functions generated from inductive predicates having neither parameters nor input arguments now take a unit element as an argument, otherwise the generated code would be ill-formed.
2007-07-11 berghofe 2007-07-11 Improved code generator for Collect.
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax