src/HOL/Sum_Type.thy
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 ***