src/HOL/Tools/datatype_abs_proofs.ML
2007-08-24 haftmann 2007-08-24 overloaded definitions accompanied by explicit constants
2007-08-20 haftmann 2007-08-20 using canonical instantiation interface
2007-08-10 haftmann 2007-08-10 ClassPackage renamed to Class
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-05-17 haftmann 2007-05-17 abstract size function in hologic.ML
2007-04-24 berghofe 2007-04-24 case constants are now authentic.
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-12-01 haftmann 2006-12-01 slight cleanup in hologic.ML
2006-11-26 wenzelm 2006-11-26 InductivePackage.add_inductive_global;
2006-11-18 haftmann 2006-11-18 added instance for class size
2006-11-14 wenzelm 2006-11-14 InductivePackage.add_inductive_i: canonical argument order;
2006-11-10 wenzelm 2006-11-10 simplified LocalTheory.exit;
2006-10-13 berghofe 2006-10-13 Adapted to new inductive definition package.
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
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-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-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
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-01-24 berghofe 2005-01-24 Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-21 berghofe 2004-05-21 Added more flexible parse / print translations for case expressions.
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-02-20 berghofe 2002-02-20 Removed superfluous lookup of theorems in Relation.thy
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-14 wenzelm 2001-11-14 inductive: removed con_defs;
2001-10-27 wenzelm 2001-10-27 hardwire qualified const names;
2001-10-14 wenzelm 2001-10-14 ObjectLogic.atomize_tac;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-08-31 wenzelm 2001-08-31 tuned headers;
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-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-08-30 berghofe 2000-08-30 Improved names for size function.
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-03-28 nipkow 2000-03-28 added weak_case_cong feature
2000-03-15 berghofe 2000-03-15 - Fixed bug in prove_casedist_thms (proof failed because of name clashes) - 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-10-21 wenzelm 1999-10-21 proper handling of axioms / defs;
1999-10-04 wenzelm 1999-10-04 eliminated ap/app;
1999-08-17 berghofe 1999-08-17 Tuned some comments.
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-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-09-26 berghofe 1998-09-26 Package now chooses type variable names more carefully to avoid clashes with user-supplied type variable names.