src/HOL/Inductive.thy
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