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
|
file |
diff |
annotate
|
Fri, 08 May 2009 13:34:27 +0200 |
haftmann |
localized (complete) partial order classes
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
Sun, 22 Jun 2008 23:08:32 +0200 |
huffman |
cleaned up some proofs;
|
file |
diff |
annotate
|
Fri, 20 Jun 2008 17:58:16 +0200 |
huffman |
tuned
|
file |
diff |
annotate
|
Wed, 18 Jun 2008 23:07:30 +0200 |
huffman |
replace preorder class with locale
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 00:27:16 +0100 |
huffman |
make preorder locale into a superclass of class po
|
file |
diff |
annotate
|
Thu, 17 Jan 2008 21:44:19 +0100 |
huffman |
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
|
file |
diff |
annotate
|
Mon, 14 Jan 2008 03:56:31 +0100 |
huffman |
use new-style class for po
|
file |
diff |
annotate
|
Thu, 10 Jan 2008 05:11:09 +0100 |
huffman |
new lemmas max_in_chainI, max_in_chainD
|
file |
diff |
annotate
|
Fri, 04 Jan 2008 23:56:47 +0100 |
huffman |
cleaned up some proofs
|
file |
diff |
annotate
|
Fri, 04 Jan 2008 00:54:12 +0100 |
huffman |
add new is_ub lemmas; clean up directed_finite proofs
|
file |
diff |
annotate
|
Thu, 03 Jan 2008 22:08:54 +0100 |
huffman |
add lub_maximal lemmas;
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 18:23:45 +0100 |
huffman |
added new lemmas
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 16:37:27 +0100 |
huffman |
new is_ub lemmas; new lub syntax for set image
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 16:17:49 +0100 |
huffman |
new section for directed sets
|
file |
diff |
annotate
|
Tue, 18 Dec 2007 19:15:31 +0100 |
huffman |
rearrange into subsections
|
file |
diff |
annotate
|
Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
Wed, 26 Sep 2007 20:27:55 +0200 |
haftmann |
moved Finite_Set before Datatype
|
file |
diff |
annotate
|
Wed, 06 Jun 2007 23:06:29 +0200 |
huffman |
use new-style class for sq_ord; rename op << to sq_le
|
file |
diff |
annotate
|
Sun, 26 Nov 2006 18:07:16 +0100 |
wenzelm |
updated (binder) syntax/notation;
|
file |
diff |
annotate
|
Thu, 28 Sep 2006 23:42:43 +0200 |
wenzelm |
fixed translations: CONST;
|
file |
diff |
annotate
|
Fri, 12 May 2006 04:20:02 +0200 |
huffman |
add new finite chain theorems
|
file |
diff |
annotate
|
Sun, 19 Feb 2006 02:11:27 +0100 |
huffman |
use minimal imports
|
file |
diff |
annotate
|
Wed, 11 Jan 2006 03:10:04 +0100 |
huffman |
add transitivity rules
|
file |
diff |
annotate
|
Fri, 04 Nov 2005 22:27:40 +0100 |
huffman |
cleaned up
|
file |
diff |
annotate
|
Thu, 03 Nov 2005 00:16:09 +0100 |
huffman |
cleaned up; chain_const and thelub_const are simp rules
|
file |
diff |
annotate
|
Mon, 10 Oct 2005 03:47:00 +0200 |
huffman |
cleaned up; renamed "Porder.op <<" to "Porder.<<"
|
file |
diff |
annotate
|
Tue, 13 Sep 2005 23:30:01 +0200 |
huffman |
add theorem chain_const
|
file |
diff |
annotate
|