src/HOL/Inductive.thy
2007-10-04 haftmann 2007-10-04 tuned datatype_codegen setup
2007-09-26 wenzelm 2007-09-26 removed dead code;
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 separated code for inductive sequences from inductive_codegen.ML
2007-08-20 nipkow 2007-08-20 Final mods for list comprehension
2007-07-11 berghofe 2007-07-11 Added new package for inductive sets.
2007-07-10 haftmann 2007-07-10 clarified import
2007-07-03 nipkow 2007-07-03 Fixed problem with patterns in lambdas
2007-07-02 nipkow 2007-07-02 Added pattern maatching for lambda abstraction
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-05-09 haftmann 2007-05-09 moved recfun_codegen.ML to Code_Generator.thy
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-24 berghofe 2007-04-24 Added datatype_case.
2007-01-31 haftmann 2007-01-31 dropped lemma duplicates in HOL.thy
2006-10-13 berghofe 2006-10-13 Added new package for inductive definitions, moved old package to old_inductive_package.ML
2006-09-19 haftmann 2006-09-19 added auxiliary lemma for code generation 2
2006-05-09 haftmann 2006-05-09 added DatatypeHooks
2005-12-22 wenzelm 2005-12-22 updated auxiliary facts for induct method;
2005-08-03 avigad 2005-08-03 import FixedPoint instead of Gfp
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-11-13 berghofe 2002-11-13 Added InductiveRealizer package.
2002-08-07 berghofe 2002-08-07 Added file Tools/datatype_realizer.ML
2002-02-21 wenzelm 2002-02-21 include theory Record (tuned dependencies);
2001-12-10 berghofe 2001-12-10 Moved code generator setup from Recdef to Inductive.
2001-11-03 wenzelm 2001-11-03 tuned;
2001-10-31 wenzelm 2001-10-31 use induct_rulify2;
2001-10-18 wenzelm 2001-10-18 moved InductMethod.setup to theory HOL;
2001-10-04 wenzelm 2001-10-04 generic induct_method.ML; tuned;
2001-07-22 wenzelm 2001-07-22 tuned;
2001-07-20 wenzelm 2001-07-20 private "myinv" (uses "The" instead of "Eps");
2001-05-22 berghofe 2001-05-22 Inductive definitions are now introduced earlier in the theory hierarchy.
2001-01-30 oheimb 2001-01-30 added if_def2
2000-12-22 wenzelm 2000-12-22 added inductive_conj;
2000-11-10 wenzelm 2000-11-10 simplified atomize; added inductive_rulify2 (to accomodate malformed induction rules);
2000-11-06 wenzelm 2000-11-06 inductive_atomize, inductive_rulify;
2000-10-23 wenzelm 2000-10-23 declare trancl rules;
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-03-15 berghofe 2000-03-15 Added setup for primrec theory data.
2000-03-04 wenzelm 2000-03-04 require NatDef;
2000-02-27 wenzelm 2000-02-27 early setup of induct_method;
1999-10-05 berghofe 1999-10-05 Monotonicity rules for inductive definitions can now be added to a theory via attribute "mono".
1999-10-04 wenzelm 1999-10-04 load / setup datatype package;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-04-16 wenzelm 1999-04-16 'HOL/inductive' theory data;
1998-07-01 wenzelm 1998-07-01 tuned Inductive.thy;
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1996-07-15 paulson 1996-07-15 New dummy .thy files to document dependencies
1995-07-25 lcp 1995-07-25 Includes Sum.thy as a parent for mutual recursion
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application