src/HOL/Sum_Type.thy
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
2014-02-12 blanchet 2014-02-12 se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets
2013-08-13 kuncar 2013-08-13 move useful lemmas to Main
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-10-18 huffman 2011-10-18 hide typedef-generated constants Product_Type.prod and Sum_Type.sum
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 replace `type_mapper` by the more adequate `type_lifting`
2010-11-18 haftmann 2010-11-18 mapper for sum type
2010-10-29 nipkow 2010-10-29 hide Sum_Type.Plus
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-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
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;
2009-12-04 haftmann 2009-12-04 tuned whitespace
2009-11-27 haftmann 2009-11-27 modernized; dropped ancient constant Part
2009-11-25 haftmann 2009-11-25 centralized sum type matter in Sum_Type.thy
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
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-07 haftmann 2008-10-07 arbitrary is undefined
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2007-12-05 haftmann 2007-12-05 simplified infrastructure for code generator operational equality
2007-05-06 haftmann 2007-05-06 tuned
2007-04-10 krauss 2007-04-10 Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
2007-03-09 haftmann 2007-03-09 *** empty log message ***
2006-11-22 haftmann 2006-11-22 dropped eq const
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-09-19 haftmann 2006-09-19 added operational equality
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-02-10 haftmann 2006-02-10 improved code generator devarification
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-08-06 nipkow 2005-08-06 new lemma
2004-12-09 paulson 2004-12-09 converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
2001-09-27 wenzelm 2001-09-27 eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2000-10-12 nipkow 2000-10-12 *** empty log message ***