src/HOL/Typedef.thy
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-06-20 huffman 2008-06-20 add lemma Abs_image
2008-05-07 berghofe 2008-05-07 Deleted instantiation "set :: (type) itself".
2008-02-26 haftmann 2008-02-26 class itself works around a problem with class interpretation in class finite
2007-12-05 haftmann 2007-12-05 interpretation of typedefs
2007-08-14 huffman 2007-08-14 remove redundant assumption from Rep_range lemma
2007-07-10 haftmann 2007-07-10 removed proof dependency on transitivity theorems
2007-06-20 nipkow 2007-06-20 added lemmas
2007-06-05 haftmann 2007-06-05 merged Code_Generator.thy into HOL.thy
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2006-08-29 haftmann 2006-08-29 added typecopy_package
2006-04-24 haftmann 2006-04-24 seperated typedef codegen from main code
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-10-26 berghofe 2004-10-26 Added setup for code generator.
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2002-07-24 wenzelm 2002-07-24 simplified locale predicates;
2002-07-24 wenzelm 2002-07-24 predicate defs via locales;
2001-11-03 wenzelm 2001-11-03 tuned;
2001-10-30 wenzelm 2001-10-30 lemma Least_mono moved from Typedef.thy to Set.thy;
2001-10-28 wenzelm 2001-10-28 converted theory "Set";
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-13 wenzelm 2001-10-13 tuned;
2001-10-03 wenzelm 2001-10-03 Tools/induct_attrib.ML now part of Pure;
2001-10-03 wenzelm 2001-10-03 moved linorder_cases to theory Ord;
2001-09-27 wenzelm 2001-09-27 renamed theory "subset" to "Typedef";