src/HOL/Tools/datatype_rep_proofs.ML
2006-04-06 haftmann 2006-04-06 cleanup in datatype package
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-12-02 haftmann 2005-12-02 introduced new map2, fold
2005-12-01 haftmann 2005-12-01 oriented pairs theory * 'a to 'a * theory
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
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-05 wenzelm 2005-09-05 curried_lookup/update;
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 Context.theory_name;
2005-06-05 wenzelm 2005-06-05 Type.freeze;
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.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-12-09 paulson 2004-12-09 converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
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.
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-07-10 berghofe 2002-07-10 Simplified proof of induction rule for datatypes involving function types.
2002-02-21 wenzelm 2002-02-21 clarified internal theory dependencies;
2001-11-14 wenzelm 2001-11-14 inductive: removed con_defs;
2001-10-27 wenzelm 2001-10-27 hardwire qualified const names;
2001-10-26 berghofe 2001-10-26 Fixed several bugs concerning arbitrarily branching datatypes.
2001-10-18 wenzelm 2001-10-18 sane internal interface for add_typedef(_i);
2001-10-17 wenzelm 2001-10-17 improved internal interface of typedef;
2001-10-16 wenzelm 2001-10-16 ignore typedef result;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-08-31 wenzelm 2001-08-31 tuned headers;
2001-08-07 berghofe 2001-08-07 - Fixed bug in isomorphism proofs (caused by migration from SOME to THE) - Funs_rangeE now requires function g to be injective
2001-07-20 wenzelm 2001-07-20 replaced "Eps" by "The";
2001-01-16 wenzelm 2001-01-16 proper induction rule for arbitrarily branching datatype;
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-03-15 berghofe 2000-03-15 Now returns theorems with correct names in derivations.
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.; proper handling of case names;
2000-02-27 wenzelm 2000-02-27 HOLogic.dest_conj;
1999-11-11 paulson 1999-11-11 new-style infix declaration for "image"
1999-10-21 wenzelm 1999-10-21 proper handling of axioms / defs;
1999-10-04 wenzelm 1999-10-04 eliminated ap/app;
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-08-19 berghofe 1999-08-19 Moved sum_case stuff from Sum to Datatype.
1999-08-18 berghofe 1999-08-18 Renamed sum_case to basic_sum_case.
1999-08-17 berghofe 1999-08-17 Tuned some comments.
1999-08-12 berghofe 1999-08-12 Tuned.
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-04-27 wenzelm 1999-04-27 adapted add_inductive;
1999-04-14 wenzelm 1999-04-14 tuned messages;
1999-04-14 wenzelm 1999-04-14 intrs: provide names and atts;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-02-03 paulson 1999-02-03 inj is now a translation of inj_on
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-10-20 wenzelm 1998-10-20 quiet proofs;
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-09-24 oheimb 1998-09-24 renamed mk_meta_eq to mk_eq
1998-08-12 oheimb 1998-08-12 renamed mk_meta_eq to meta_eq
1998-07-30 berghofe 1998-07-30 Deleted obsolete comments.
1998-07-24 berghofe 1998-07-24 New datatype definition package