src/HOL/Typedef.thy
Thu, 14 Mar 2019 16:55:06 +0100 wenzelm more specific keyword kinds;
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Mon, 11 Jul 2016 10:43:54 +0200 wenzelm more indentation for quasi_command keywords;
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Thu, 03 Sep 2015 17:14:57 +0200 wenzelm misc tuning and modernization;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Mon, 08 Sep 2014 23:04:18 +0200 blanchet added flag to 'typedef' to allow concealed definitions
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header;
Tue, 08 Feb 2011 20:59:12 +0100 wenzelm discontinued obsolete alias HOL.thy for @{theory HOL} in ML;
Tue, 17 Aug 2010 16:44:24 +0200 haftmann dropped SML typedef_codegen: does not fit to code equations for record operations any longer
Thu, 12 Aug 2010 17:56:41 +0200 haftmann group record-related ML files
Tue, 20 Jul 2010 23:09:49 +0200 wenzelm discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Tue, 03 Feb 2009 21:26:21 +0100 haftmann handling type classes without parameters
Wed, 21 Jan 2009 23:40:23 +0100 haftmann no base sort in class import
Thu, 11 Dec 2008 00:42:52 +0100 wenzelm misc tuning and modernisation;
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Mon, 29 Sep 2008 10:58:01 +0200 wenzelm LocalTheory.exit_global;
Tue, 02 Sep 2008 16:55:33 +0200 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Fri, 20 Jun 2008 19:57:45 +0200 huffman add lemma Abs_image
Wed, 07 May 2008 10:56:50 +0200 berghofe Deleted instantiation "set :: (type) itself".
Tue, 26 Feb 2008 20:38:16 +0100 haftmann class itself works around a problem with class interpretation in class finite
Wed, 05 Dec 2007 14:15:48 +0100 haftmann interpretation of typedefs
Tue, 14 Aug 2007 23:05:55 +0200 huffman remove redundant assumption from Rep_range lemma
Tue, 10 Jul 2007 17:30:51 +0200 haftmann removed proof dependency on transitivity theorems
Wed, 20 Jun 2007 14:38:24 +0200 nipkow added lemmas
Tue, 05 Jun 2007 15:16:08 +0200 haftmann merged Code_Generator.thy into HOL.thy
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Tue, 29 Aug 2006 14:31:13 +0200 haftmann added typecopy_package
Mon, 24 Apr 2006 16:37:52 +0200 haftmann seperated typedef codegen from main code
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 26 Oct 2004 16:31:09 +0200 berghofe Added setup for code generator.
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Wed, 24 Jul 2002 22:15:55 +0200 wenzelm simplified locale predicates;
Wed, 24 Jul 2002 00:10:52 +0200 wenzelm predicate defs via locales;
Sat, 03 Nov 2001 01:33:54 +0100 wenzelm tuned;
Tue, 30 Oct 2001 13:43:26 +0100 wenzelm lemma Least_mono moved from Typedef.thy to Set.thy;
Sun, 28 Oct 2001 22:59:12 +0100 wenzelm converted theory "Set";
Sun, 14 Oct 2001 22:08:29 +0200 wenzelm moved rulify to ObjectLogic;
Sat, 13 Oct 2001 21:43:00 +0200 wenzelm tuned;
Wed, 03 Oct 2001 21:03:05 +0200 wenzelm Tools/induct_attrib.ML now part of Pure;
Wed, 03 Oct 2001 20:54:05 +0200 wenzelm moved linorder_cases to theory Ord;
Thu, 27 Sep 2001 22:26:00 +0200 wenzelm renamed theory "subset" to "Typedef";
less more (0) tip