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