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