src/HOL/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