src/HOL/Tools/datatype_package.ML
2008-06-19 wenzelm 2008-06-19 export read_typ/cert_typ -- version with regular context operations;
2008-06-18 wenzelm 2008-06-18 eliminated old Sign.read_term/Thm.read_cterm etc.;
2008-06-10 wenzelm 2008-06-10 moved case_tac/induct_tac to induct_tacs.ML -- no longer hardwired into datatype package;
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2008-06-09 wenzelm 2008-06-09 signature cleanup -- no pervasives anymore;
2008-05-28 haftmann 2008-05-28 moved distinctness_limit to datatype_rep_proofs.ML
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-03 berghofe 2008-04-03 Deleted code for axiomatic introduction of datatypes. Instead, the package now uses SkipProof.prove rather than Goal.prove to do proofs.
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-14 haftmann 2008-03-14 added combinator for interpretation of construction of datatype
2008-02-22 haftmann 2008-02-22 added first version of datatype antiquotation
2008-02-18 haftmann 2008-02-18 tuned
2008-01-10 berghofe 2008-01-10 Eliminated DatatypeAux.dest_TFree to avoid clashes with Term.dest_TFree.
2007-12-17 berghofe 2007-12-17 - Removed redundant head_len field in datatype_info - Added new alt_names field in datatype_info
2007-12-05 haftmann 2007-12-05 interface and distinct simproc tuned
2007-11-28 wenzelm 2007-11-28 ObjectLogic.typedecl;
2007-11-23 haftmann 2007-11-23 separated typedecl module, providing typedecl command with interpretation
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-30 wenzelm 2007-09-30 Sign.add_consts_authentic: tags (Markup.property list);
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-25 wenzelm 2007-09-25 simplified interpretation setup;
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-09-15 haftmann 2007-09-15 clarified class interfaces and internals
2007-08-24 haftmann 2007-08-24 overloaded definitions accompanied by explicit constants
2007-08-20 nipkow 2007-08-20 Final mods for list comprehension
2007-08-20 haftmann 2007-08-20 using canonical instantiation interface
2007-08-10 haftmann 2007-08-10 ClassPackage renamed to Class
2007-07-31 wenzelm 2007-07-31 replaced dtK ref by datatype_distinctness_limit configuration option;
2007-05-17 haftmann 2007-05-17 abstract size function in hologic.ML
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-24 berghofe 2007-04-24 - Moved parse / print translations for case to datatype_case.ML - Added new functions datatype_of_constr and datatype_of_case to retrieve datatype corresponding to name of constructor or case combinator.
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field; renamed Variable.importT to importT_thms;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-03-20 haftmann 2007-03-20 switched exception from arbitrary to undefined
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context;
2006-12-07 paulson 2006-12-07 Removal of theorem tagging, which the ATP linkup no longer requires,
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-22 haftmann 2006-11-22 no explicit check for theory Nat
2006-11-18 haftmann 2006-11-18 added instance for class size
2006-11-14 wenzelm 2006-11-14 incorporated IsarThy into IsarCmd;
2006-11-08 wenzelm 2006-11-08 case_tr': proper handling of authentic consts;
2006-11-08 haftmann 2006-11-08 renamed DatatypeHooks.invoke to all
2006-11-08 wenzelm 2006-11-08 removed theory NatArith (now part of Nat);
2006-11-05 wenzelm 2006-11-05 case_tr: do not intern already internal consts;
2006-10-31 haftmann 2006-10-31 cleaned up
2006-10-16 haftmann 2006-10-16 slight cleanup
2006-10-01 wenzelm 2006-10-01 removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-09-26 haftmann 2006-09-26 handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
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;