src/HOL/Inductive.thy
2010-09-28 haftmann 2010-09-28 dropped old primrec package
2010-06-10 haftmann 2010-06-10 moved inductive_codegen to place where product type is available; tuned structure name
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-30 haftmann 2009-11-30 merged
2009-11-27 haftmann 2009-11-27 renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
2009-11-25 haftmann 2009-11-25 bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
2009-11-27 berghofe 2009-11-27 Streamlined setup for monotonicity rules (no longer requires classical rules).
2009-09-23 haftmann 2009-09-23 merged
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-23 haftmann 2009-09-23 stripped legacy ML bindings
2009-09-16 haftmann 2009-09-16 Inter and Union are mere abbreviations for Inf and Sup
2009-07-06 haftmann 2009-07-06 moved Inductive.myinv to Fun.inv; tuned
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-10 haftmann 2009-06-10 separate directory for datatype package
2008-12-31 wenzelm 2008-12-31 eliminated OldTerm.add_term_free_names;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-05-07 berghofe 2008-05-07 Instantiated some rules to avoid problems with HO unification.
2008-01-30 haftmann 2008-01-30 Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
2007-12-06 haftmann 2007-12-06 added new primrec package
2007-12-05 haftmann 2007-12-05 simplified infrastructure for code generator operational equality
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-10-08 haftmann 2007-10-08 integrated FixedPoint into Inductive
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.