src/HOL/Typedef.thy
2012-08-22 wenzelm prefer ML_file over old uses;
2012-03-15 wenzelm declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm declare minor keywords via theory header;
2011-02-08 wenzelm discontinued obsolete alias HOL.thy for @{theory HOL} in ML;
2010-08-17 haftmann dropped SML typedef_codegen: does not fit to code equations for record operations any longer
2010-08-12 haftmann group record-related ML files
2010-07-20 wenzelm discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
2009-06-19 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
2009-02-03 haftmann handling type classes without parameters
2009-01-21 haftmann no base sort in class import
2008-12-10 wenzelm misc tuning and modernisation;
2008-12-04 haftmann cleaned up binding module and related code
2008-09-29 wenzelm LocalTheory.exit_global;
2008-09-02 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 wenzelm explicit type Name.binding for higher-specification elements;
2008-06-20 huffman add lemma Abs_image
2008-05-07 berghofe Deleted instantiation "set :: (type) itself".
2008-02-26 haftmann class itself works around a problem with class interpretation in class finite
2007-12-05 haftmann interpretation of typedefs
2007-08-14 huffman remove redundant assumption from Rep_range lemma
2007-07-10 haftmann removed proof dependency on transitivity theorems
2007-06-20 nipkow added lemmas
2007-06-05 haftmann merged Code_Generator.thy into HOL.thy
2007-05-06 wenzelm simplified DataFun interfaces;
2006-08-29 haftmann added typecopy_package
2006-04-24 haftmann seperated typedef codegen from main code
2005-06-17 haftmann migrated theory headers to new format
2004-10-26 berghofe Added setup for code generator.
2004-08-18 nipkow import -> imports
2004-08-16 nipkow New theory header syntax.
2002-07-24 wenzelm simplified locale predicates;
2002-07-23 wenzelm predicate defs via locales;
2001-11-03 wenzelm tuned;
2001-10-30 wenzelm lemma Least_mono moved from Typedef.thy to Set.thy;
2001-10-28 wenzelm converted theory "Set";
2001-10-14 wenzelm moved rulify to ObjectLogic;
2001-10-13 wenzelm tuned;
2001-10-03 wenzelm Tools/induct_attrib.ML now part of Pure;
2001-10-03 wenzelm moved linorder_cases to theory Ord;
2001-09-27 wenzelm renamed theory "subset" to "Typedef";
less more (0) tip