src/HOL/Inductive.thy
2016-10-01 wenzelm 2016-10-01 Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
2016-10-01 wenzelm 2016-10-01 clarified lfp/gfp statements and proofs;
2016-10-01 wenzelm 2016-10-01 added lemma;
2016-09-13 traytel 2016-09-13 don't expose internal construction in the coinduction rule for mutual coinductive predicates
2016-08-02 wenzelm 2016-08-02 misc tuning and modernization;
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-05 wenzelm 2016-07-05 misc tuning and modernization;
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-28 wenzelm 2015-12-28 prefer symbols for "Union", "Inter";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
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