src/HOL/Tools/datatype_aux.ML
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-05 berghofe 2005-12-05 Added store_thmss_atts to signature again.
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-11-10 wenzelm 2005-11-10 renamed Thm.cgoal_of to Thm.cprem_of;
2005-11-07 berghofe 2005-11-07 New function store_thmss_atts.
2005-11-02 huffman 2005-11-02 fix spelling
2005-10-28 wenzelm 2005-10-28 Logic.unprotect;
2005-09-19 haftmann 2005-09-19 introduced AList module
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-07-22 berghofe 2005-07-22 Tuned comment.
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.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-12-07 webertj 2004-12-07 comment added
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-08 berghofe 2004-06-08 Added exception Datatype_Empty.
2004-04-26 wenzelm 2004-04-26 use Syntax.is_identifier;
2002-11-13 berghofe 2002-11-13 name_of_type now replaces non-identifiers by dummy names.
2002-10-10 berghofe 2002-10-10 Reimplemented parts of datatype package dealing with datatypes involving function types. Now also supports functions with more than one argument.
2001-08-31 wenzelm 2001-08-31 tuned headers;
2000-10-02 wenzelm 2000-10-02 info: weak_case_cong;
2000-08-30 berghofe 2000-08-30 New function name_of_typ.
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.; added store_thms_atts;
2000-03-10 wenzelm 2000-03-10 type descr;
2000-03-01 wenzelm 2000-03-01 tuned;
2000-02-27 wenzelm 2000-02-27 HOLogic.dest_conj;
1999-07-16 berghofe 1999-07-16 - Datatype package now also supports arbitrarily branching datatypes (using function types). - Added new simplification procedure for proving distinctness of constructors. - dtK is now a reference.
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-16 wenzelm 1998-11-16 Attribute.tthms_of;
1998-10-16 berghofe 1998-10-16 - Changed structure of name spaces - Proofs for datatypes with unneeded parameters are working now - added additional parameter flat_names - added quiet_mode flag
1998-07-24 berghofe 1998-07-24 New datatype definition package