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
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-25 berghofe 2007-04-25 Moved function params_of to inductive_package.ML.
2007-04-13 berghofe 2007-04-13 Removed erroneous application of rev in get_clauses that caused introduction rules taken from the InductivePackage database to be in the wrong order.
2007-04-12 haftmann 2007-04-12 canonical merge operations
2007-03-31 berghofe 2007-03-31 Fixed bug in dest_prem: premises of the form "p x_1 ... x_n" (where p is a variable) are now treated as side conditions if p is not in the list of (global) parameters.
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-10-13 berghofe 2006-10-13 Moved old inductive package to old_inductive_package.ML
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-12 wenzelm 2006-06-12 tuned Seq/Envir/Unify interfaces;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-12 wenzelm 2006-02-12 simplified TableFun.join;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 replaced Symtab.merge_multi by local merge_rules;