2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-03 hoelzl 2015-07-03 add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-05-04 hoelzl 2015-05-04 strengthened lfp_ordinal_induct; added dual gfp variant
2015-05-04 hoelzl 2015-05-04 add rules for least/greatest fixed point calculus
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-05 blanchet 2014-09-05 fixed infinite loops in 'register' functions + more uniform API
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-03-14 wenzelm 2014-03-14 discontinued somewhat pointless "thy_script" keyword kind;
2014-02-20 noschinl 2014-02-20 less flex-flex pairs
2014-02-19 blanchet 2014-02-19 moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
2014-02-17 blanchet 2014-02-17 renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
2013-12-02 blanchet 2013-12-02 generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
2013-11-12 blanchet 2013-11-12 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-04-10 wenzelm 2013-04-10 tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side; declare command "print_case_translations" where it is actually defined;
2013-04-06 traytel 2013-04-06 disallow coercions to interfere with case translations
2013-04-05 traytel 2013-04-05 allow redundant cases in the list comprehension translation
2013-04-05 traytel 2013-04-05 special constant to prevent eta-contraction of the check-phase syntax of case translations
2013-01-22 traytel 2013-01-22 separate data used for case translation from the datatype package
2013-01-22 berghofe 2013-01-22 case translations performed in a separate check phase (with adjustments by traytel)
2012-11-30 wenzelm 2012-11-30 added 'print_inductives' command;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-19 haftmann 2012-07-19 removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2011-12-28 wenzelm 2011-12-28 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs;
2011-12-17 wenzelm 2011-12-17 clarified modules that contribute to datatype package;
2011-12-16 wenzelm 2011-12-16 prefer Name.context operations;
2011-12-16 wenzelm 2011-12-16 clarified modules that contribute to datatype package;
2011-12-15 wenzelm 2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-15 wenzelm 2011-12-15 separate rep_datatype.ML; tuned signature;
2011-09-10 haftmann 2011-09-10 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
2011-06-27 krauss 2011-06-27 new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor; renamed old version to info_of_constr_permissive, reflecting its semantics
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2010-12-08 haftmann 2010-12-08 tuned
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