| Fri, 29 Oct 2010 16:24:07 -0700 |
huffman |
simplify proof of typedef_cont_Abs
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 13:54:18 -0700 |
huffman |
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 06:58:45 -0700 |
huffman |
remove finite_po class
|
file |
diff |
annotate
|
| Sun, 17 Oct 2010 09:53:47 -0700 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 12:52:51 -0700 |
huffman |
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
|
file |
diff |
annotate
|
| Sun, 21 Jun 2009 08:38:58 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| 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
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 12:07:34 +0200 |
haftmann |
adapted to class instantiation compliance
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 19:59:00 +0200 |
huffman |
moved Abs_image to Typedef.thy; prove finite_UNIV outside the 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, 31 Jan 2008 21:48:14 +0100 |
huffman |
add lemma cpo_lubI
|
file |
diff |
annotate
|
| Fri, 18 Jan 2008 20:31:11 +0100 |
huffman |
pcpodef generates strict_iff lemmas
|
file |
diff |
annotate
|
| Fri, 18 Jan 2008 20:22:07 +0100 |
huffman |
change lemma admD to rule_format
|
file |
diff |
annotate
|
| Thu, 17 Jan 2008 00:51:20 +0100 |
huffman |
change class axiom chfin to rule_format
|
file |
diff |
annotate
|
| Fri, 04 Jan 2008 00:01:02 +0100 |
huffman |
new instance proofs for classes finite_po, chfin, flat
|
file |
diff |
annotate
|
| Thu, 31 May 2007 14:01:58 +0200 |
wenzelm |
moved HOLCF tools to canonical place;
|
file |
diff |
annotate
|
| Mon, 01 May 2006 01:21:23 +0200 |
huffman |
add theorem typdef_flat
|
file |
diff |
annotate
|
| Tue, 11 Oct 2005 23:23:39 +0200 |
huffman |
added theorem typedef_compact
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 04:00:40 +0200 |
huffman |
added theorem typedef_chfin
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 18:24:29 +0200 |
huffman |
cleaned up; renamed some theorems
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 18:20:08 +0200 |
huffman |
use theorems ch2ch_cont, cont2contlubE
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 00:04:31 +0200 |
huffman |
renamed from TypedefPcpo.thy;
|
file |
diff |
annotate
|