src/HOLCF/One.thy
Sat, 13 Mar 2010 22:00:34 -0800 huffman declare case_names for various induction rules
Wed, 03 Mar 2010 00:33:02 +0100 wenzelm cleanup type translations;
Fri, 08 May 2009 16:19:51 -0700 huffman rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
Fri, 10 Apr 2009 17:39:53 -0700 huffman domain package: simplify internal proofs of con_rews
Thu, 18 Dec 2008 11:00:13 -0800 huffman constdefs -> definition
Tue, 16 Dec 2008 21:31:55 -0800 huffman remove cvs Id tags
Fri, 20 Jun 2008 18:00:55 +0200 huffman added some lemmas; tuned proofs
Sun, 21 Oct 2007 14:21:48 +0200 wenzelm modernized specifications ('definition', 'abbreviation', 'notation');
Mon, 07 Nov 2005 23:30:49 +0100 huffman add case syntax for type one
Thu, 03 Nov 2005 01:44:27 +0100 huffman add constant one_when; LAM pattern for ONE
Wed, 12 Oct 2005 03:01:09 +0200 huffman added compactness theorems
Thu, 07 Jul 2005 20:41:12 +0200 huffman cleaned up
Wed, 25 May 2005 09:44:34 +0200 wenzelm removed LICENCE note -- everything is subject to Isabelle licence as
Fri, 04 Mar 2005 23:23:47 +0100 huffman fix headers
Fri, 04 Mar 2005 23:12:36 +0100 huffman converted to new-style theories, and combined numbered files
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sat, 03 Nov 2001 01:41:26 +0100 wenzelm GPLed;
Fri, 26 Sep 1997 10:12:04 +0200 wenzelm eliminated rules;
Mon, 17 Feb 1997 10:57:11 +0100 slotosch Changes of HOLCF from Oscar Slotosch:
Fri, 29 Nov 1996 12:15:33 +0100 oheimb renamed is_flat to flat,
Tue, 06 Feb 1996 12:42:31 +0100 clasohm expanded tabs
Fri, 06 Oct 1995 17:25:24 +0100 regensbu added 8bit pragmas
Thu, 29 Jun 1995 16:28:40 +0200 regensbu The curried version of HOLCF is now just called HOLCF. The old
Thu, 06 Oct 1994 18:40:18 +0100 nipkow New version
Wed, 19 Jan 1994 17:35:01 +0100 nipkow Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
less more (0) tip