src/HOL/Typedef.thy
2016-07-11 wenzelm 2016-07-11 more indentation for quasi_command keywords;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-09-03 wenzelm 2015-09-03 misc tuning and modernization;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-08 blanchet 2014-09-08 added flag to 'typedef' to allow concealed definitions
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2011-02-08 wenzelm 2011-02-08 discontinued obsolete alias HOL.thy for @{theory HOL} in ML;
2010-08-17 haftmann 2010-08-17 dropped SML typedef_codegen: does not fit to code equations for record operations any longer
2010-08-12 haftmann 2010-08-12 group record-related ML files
2010-07-20 wenzelm 2010-07-20 discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-02-03 haftmann 2009-02-03 handling type classes without parameters
2009-01-21 haftmann 2009-01-21 no base sort in class import
2008-12-11 wenzelm 2008-12-11 misc tuning and modernisation;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-29 wenzelm 2008-09-29 LocalTheory.exit_global;
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";