src/HOLCF/Porder.thy
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, 08 May 2009 13:34:27 +0200 haftmann localized (complete) partial order classes
Wed, 21 Jan 2009 23:40:23 +0100 haftmann no base sort in class import
Tue, 16 Dec 2008 21:31:55 -0800 huffman remove cvs Id tags
Sun, 22 Jun 2008 23:08:32 +0200 huffman cleaned up some proofs;
Fri, 20 Jun 2008 17:58:16 +0200 huffman tuned
Wed, 18 Jun 2008 23:07:30 +0200 huffman replace preorder class with locale
Thu, 27 Mar 2008 00:27:16 +0100 huffman make preorder locale into a superclass of class po
Thu, 17 Jan 2008 21:44:19 +0100 huffman rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
Mon, 14 Jan 2008 03:56:31 +0100 huffman use new-style class for po
Thu, 10 Jan 2008 05:11:09 +0100 huffman new lemmas max_in_chainI, max_in_chainD
Fri, 04 Jan 2008 23:56:47 +0100 huffman cleaned up some proofs
Fri, 04 Jan 2008 00:54:12 +0100 huffman add new is_ub lemmas; clean up directed_finite proofs
Thu, 03 Jan 2008 22:08:54 +0100 huffman add lub_maximal lemmas;
Wed, 02 Jan 2008 18:23:45 +0100 huffman added new lemmas
Wed, 02 Jan 2008 16:37:27 +0100 huffman new is_ub lemmas; new lub syntax for set image
Wed, 02 Jan 2008 16:17:49 +0100 huffman new section for directed sets
Tue, 18 Dec 2007 19:15:31 +0100 huffman rearrange into subsections
Sun, 21 Oct 2007 14:21:48 +0200 wenzelm modernized specifications ('definition', 'abbreviation', 'notation');
Wed, 26 Sep 2007 20:27:55 +0200 haftmann moved Finite_Set before Datatype
Wed, 06 Jun 2007 23:06:29 +0200 huffman use new-style class for sq_ord; rename op << to sq_le
Sun, 26 Nov 2006 18:07:16 +0100 wenzelm updated (binder) syntax/notation;
Thu, 28 Sep 2006 23:42:43 +0200 wenzelm fixed translations: CONST;
Fri, 12 May 2006 04:20:02 +0200 huffman add new finite chain theorems
Sun, 19 Feb 2006 02:11:27 +0100 huffman use minimal imports
Wed, 11 Jan 2006 03:10:04 +0100 huffman add transitivity rules
Fri, 04 Nov 2005 22:27:40 +0100 huffman cleaned up
Thu, 03 Nov 2005 00:16:09 +0100 huffman cleaned up; chain_const and thelub_const are simp rules
Mon, 10 Oct 2005 03:47:00 +0200 huffman cleaned up; renamed "Porder.op <<" to "Porder.<<"
Tue, 13 Sep 2005 23:30:01 +0200 huffman add theorem chain_const
Wed, 08 Jun 2005 00:59:46 +0200 huffman added theorems is_ub_range_shift and is_lub_range_shift
Fri, 27 May 2005 00:15:24 +0200 huffman added lemma thelub_const
Wed, 25 May 2005 09:44:34 +0200 wenzelm removed LICENCE note -- everything is subject to Isabelle licence as
Fri, 06 May 2005 03:47:44 +0200 huffman Replaced all unnecessary uses of SOME with THE or LEAST
Thu, 10 Mar 2005 20:22:45 +0100 huffman fixed filename in header
Mon, 07 Mar 2005 23:54:01 +0100 huffman added subsections and text for document generation
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
Wed, 02 Mar 2005 22:30:00 +0100 huffman converted to new-style theory
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Fri, 09 Nov 2001 00:09:47 +0100 wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
Sat, 03 Nov 2001 01:41:26 +0100 wenzelm GPLed;
Thu, 31 May 2001 16:52:32 +0200 oheimb corrected ML names of definitions
Tue, 10 Mar 1998 18:33:13 +0100 oheimb renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Mon, 17 Feb 1997 10:57:11 +0100 slotosch Changes of HOLCF from Oscar Slotosch:
Fri, 13 Dec 1996 18:45:58 +0100 oheimb adaptions for symbol font
Mon, 02 Dec 1996 12:37:15 +0100 oheimb removed 8bit sections
Fri, 29 Nov 1996 12:22:22 +0100 oheimb *** empty log message ***
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, 24 Mar 1994 13:36:34 +0100 nipkow Franz fragen
Wed, 19 Jan 1994 17:35:01 +0100 nipkow Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
less more (0) tip