src/HOL/Tools/datatype_abs_proofs.ML
2006-10-13 ago Adapted to new inductive definition package.
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-08 ago Goal.prove_global;
2006-03-10 ago renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-01-21 ago simplified type attribute;
2005-12-09 ago oriented result pairs in PureThy
2005-12-06 ago re-oriented some result tuples in PureThy
2005-12-01 ago oriented pairs theory * 'a to 'a * theory
2005-10-25 ago avoid legacy goals;
2005-10-21 ago OldGoals;
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-05 ago curried_lookup/update;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-01-24 ago Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
2004-06-21 ago Merged in license change from Isabelle2004
2004-05-21 ago Added more flexible parse / print translations for case expressions.
2002-10-10 ago Reimplemented parts of datatype package dealing with datatypes involving
2002-02-20 ago Removed superfluous lookup of theorems in Relation.thy
2001-12-01 ago renamed class "term" to "type" (actually "HOL.type");
2001-11-14 ago inductive: removed con_defs;
2001-10-27 ago hardwire qualified const names;
2001-10-14 ago ObjectLogic.atomize_tac;
2001-09-28 ago inductive: no collective atts;
2001-08-31 ago tuned headers;
2001-07-20 ago replaced "Eps" by "The";
2001-01-16 ago proper induction rule for arbitrarily branching datatype;
2000-10-13 ago *** empty log message ***
2000-10-12 ago *** empty log message ***
2000-09-15 ago renamed (most of...) the select rules
2000-08-30 ago Improved names for size function.
2000-07-13 ago adapted PureThy.add_defs_i;
2000-03-28 ago added weak_case_cong feature
2000-03-15 ago - Fixed bug in prove_casedist_thms (proof failed because of
2000-03-13 ago adapted to new PureThy.add_thms etc.;
2000-02-27 ago HOLogic.dest_conj;
1999-10-21 ago proper handling of axioms / defs;
1999-10-04 ago eliminated ap/app;
1999-08-17 ago Tuned some comments.
1999-07-16 ago - Datatype package now also supports arbitrarily branching datatypes
1999-04-27 ago adapted add_inductive;
1999-04-14 ago tuned messages;
1999-04-14 ago intrs: provide names and atts;
1999-03-17 ago Theory.sign_of;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-11-16 ago Attribute.tthms_of;
1998-10-16 ago - Changed structure of name spaces
1998-09-26 ago Package now chooses type variable names more carefully to
1998-09-24 ago renamed mk_meta_eq to mk_eq
1998-08-12 ago renamed mk_meta_eq to meta_eq
1998-07-24 ago New datatype definition package