src/HOL/Tools/datatype_package.ML
2006-09-19 haftmann 2006-09-19 code generation 2 adjustments
2006-08-03 wenzelm 2006-08-03 RuleInsts.bires_inst_tac;
2006-07-26 wenzelm 2006-07-26 Variable.import(T): result includes fixed types/terms;
2006-07-21 haftmann 2006-07-21 hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
2006-07-21 berghofe 2006-07-21 Some cases in "case ... of ..." expressions may now be omitted (internally, these cases are assigned the "undefined" value).
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 distinct simproc/simpset: proper context;
2006-06-19 wenzelm 2006-06-19 eliminated freeze/varify in favour of Variable.import/export/trade;
2006-06-13 wenzelm 2006-06-13 ProjectRule now context dependent;
2006-06-11 wenzelm 2006-06-11 avoid unqualified exception;
2006-05-24 wenzelm 2006-05-24 add_datatype_axm: finalize specified consts;
2006-05-09 haftmann 2006-05-09 added DatatypeHooks
2006-05-02 wenzelm 2006-05-02 ThyInfo.the_theory; tuned;
2006-04-06 haftmann 2006-04-06 cleanup in datatype package
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-10 haftmann 2006-02-10 improved code generator devarification
2006-02-10 wenzelm 2006-02-10 Args/Attrib syntax: Context.generic;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-07 haftmann 2006-02-07 slight improvements in code generation
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-01-31 wenzelm 2006-01-31 advanced translations: Context.generic;
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2006-01-23 paulson 2006-01-23 bugfix: induct_tac no longer raises THM "dest_state"
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-15 wenzelm 2006-01-15 classical attributes: optional weight;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-10 wenzelm 2006-01-10 generic attributes;
2006-01-09 paulson 2006-01-09 _E suffix for compatibility with AddIffs
2005-12-29 haftmann 2005-12-29 adaptions to changes in code generator
2005-12-22 wenzelm 2005-12-22 *.inducts holds all projected rules;
2005-12-21 haftmann 2005-12-21 slight improvements
2005-12-21 haftmann 2005-12-21 slight clean ups
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-01 berghofe 2005-12-01 Added new component "sorts" to record datatype_info.
2005-12-01 haftmann 2005-12-01 oriented pairs theory * 'a to 'a * theory
2005-10-28 haftmann 2005-10-28 swapped add_datatype result
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-09-20 haftmann 2005-09-20 introduced AList module in favor of assoc etc.
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-08-01 wenzelm 2005-08-01 simprocs: Simplifier.inherit_bounds;
2005-07-04 haftmann 2005-07-04 (intermediate commit)
2005-07-01 berghofe 2005-07-01 Adapted to new interface of RecfunCodegen.add.
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Sign.the_const_type; Context.exists_name;
2005-06-11 wenzelm 2005-06-11 refer to name spaces values instead of names;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src; Args.maybe;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.