src/HOL/Datatype.thy
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-11-12 blanchet 2013-11-12 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-15 haftmann 2012-04-15 centralized enriched_type declaration, thanks to in-situ available Isar commands
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-03-30 bulwahn 2011-03-30 renewing specifications in HOL: replacing types by type_synonym
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-06 haftmann 2010-12-06 moved bootstrap of type_lifting to Fun
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
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-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-12 haftmann 2009-11-12 explicit code lemmas produce nices code
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
2009-01-21 haftmann 2009-01-21 changed import hierarchy
2009-01-21 haftmann 2009-01-21 dropped ID
2008-12-27 krauss 2008-12-27 removed duplicate sum_case used only by function package; moved projections; hide (open)
2008-12-09 huffman 2008-12-09 move lemmas from Numeral_Type.thy to other theories
2008-10-24 haftmann 2008-10-24 more clever module names for code generation
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2008-09-25 haftmann 2008-09-25 discontinued special treatment of op = vs. eq_class.eq
2008-08-24 haftmann 2008-08-24 tuned import order
2008-08-11 haftmann 2008-08-11 moved class wellorder to theory Orderings
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-03-20 haftmann 2008-03-20 Product_Type.apfst and Product_Type.apsnd
2008-03-19 wenzelm 2008-03-19 eliminated change_claset/simpset;
2008-02-26 haftmann 2008-02-26 tuned proofs
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-01-05 haftmann 2008-01-05 more instantiation
2007-12-17 berghofe 2007-12-17 Removed obsolete lemma size_sum.
2007-12-05 haftmann 2007-12-05 simplified infrastructure for code generator operational equality
2007-11-30 haftmann 2007-11-30 more canonical attribute application
2007-10-04 haftmann 2007-10-04 tuned datatype_codegen setup
2007-09-26 haftmann 2007-09-26 moved Finite_Set before Datatype
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-09 haftmann 2007-08-09 re-eliminated Option.thy
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-05-09 haftmann 2007-05-09 moved recfun_codegen.ML to Code_Generator.thy
2007-04-24 berghofe 2007-04-24 Added intro / elim rules for prod_case.
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-04-11 haftmann 2007-04-11 dropped legacy ML bindings
2007-03-09 haftmann 2007-03-09 *** empty log message ***
2007-02-02 nipkow 2007-02-02 a few additions and deletions
2006-12-27 haftmann 2006-12-27 removed code generation stuff belonging to other theories
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings;
2006-11-22 haftmann 2006-11-22 dropped eq const
2006-11-18 haftmann 2006-11-18 reduced verbosity
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;