src/HOL/Sum_Type.thy
Wed, 12 Feb 2014 08:35:56 +0100 blanchet se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move useful lemmas to Main
Sat, 20 Oct 2012 09:12:16 +0200 haftmann moved quite generic material from theory Enum to more appropriate places
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Tue, 18 Oct 2011 15:19:06 +0200 huffman hide typedef-generated constants Product_Type.prod and Sum_Type.sum
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for sum type
Fri, 29 Oct 2010 17:25:22 +0200 nipkow hide Sum_Type.Plus
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Tue, 08 Jun 2010 16:37:22 +0200 haftmann tuned quotes, antiquotations and whitespace
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Fri, 04 Dec 2009 18:52:55 +0100 haftmann tuned whitespace
Fri, 27 Nov 2009 08:41:08 +0100 haftmann modernized; dropped ancient constant Part
Wed, 25 Nov 2009 11:16:58 +0100 haftmann centralized sum type matter in Sum_Type.thy
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Sat, 27 Dec 2008 17:49:15 +0100 krauss removed duplicate sum_case used only by function package;
Tue, 09 Dec 2008 15:31:38 -0800 huffman move lemmas from Numeral_Type.thy to other theories
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Tue, 10 Jun 2008 15:30:33 +0200 haftmann rep_datatype command now takes list of constructors as input arguments
Wed, 05 Dec 2007 14:15:45 +0100 haftmann simplified infrastructure for code generator operational equality
Sun, 06 May 2007 21:49:23 +0200 haftmann tuned
Tue, 10 Apr 2007 14:11:01 +0200 krauss Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
Fri, 09 Mar 2007 08:45:55 +0100 haftmann *** empty log message ***
Wed, 22 Nov 2006 10:20:12 +0100 haftmann dropped eq const
Mon, 16 Oct 2006 14:07:31 +0200 haftmann moved HOL code generator setup to Code_Generator
Tue, 19 Sep 2006 15:21:42 +0200 haftmann added operational equality
Mon, 14 Aug 2006 13:46:06 +0200 haftmann simplified code generator setup
Fri, 10 Feb 2006 09:09:07 +0100 haftmann improved code generator devarification
Tue, 16 Aug 2005 15:36:28 +0200 paulson classical rules must have names for ATP integration
Sat, 06 Aug 2005 08:16:19 +0200 nipkow new lemma
Thu, 09 Dec 2004 16:45:46 +0100 paulson converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
Thu, 27 Sep 2001 22:28:16 +0200 wenzelm eliminated theories "equalities" and "mono" (made part of "Typedef",
Tue, 09 Jan 2001 15:22:13 +0100 nipkow `` -> and ``` -> ``
Thu, 12 Oct 2000 18:44:35 +0200 nipkow *** empty log message ***
less more (0) tip