| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 02:19:53 +0200 |
huffman |
replace lub (range Y) with (LUB i. Y i)
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 23:01:09 +0200 |
huffman |
simplify profinite class axioms
|
file |
diff |
annotate
|
| Mon, 19 May 2008 23:49:20 +0200 |
huffman |
use new class package for classes profinite, bifinite; remove approx class
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:38:17 +0100 |
huffman |
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
|
file |
diff |
annotate
|
| Sat, 02 Feb 2008 03:28:36 +0100 |
huffman |
instance "*" :: (sq_ord, sq_ord) sq_ord
|
file |
diff |
annotate
|
| Fri, 01 Feb 2008 02:38:41 +0100 |
huffman |
add lemmas prod_lessI and Pair_less_iff [simp]
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 21:48:14 +0100 |
huffman |
add lemma cpo_lubI
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 21:23:14 +0100 |
huffman |
instances for class discrete_cpo
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 01:31:19 +0100 |
huffman |
new lemma is_lub_Pair; cleaned up some proofs
|
file |
diff |
annotate
|
| Thu, 17 Jan 2008 00:51:20 +0100 |
huffman |
change class axiom chfin to rule_format
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 02:18:01 +0100 |
huffman |
declare cpair_strict [simp]
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 21:16:06 +0100 |
huffman |
add bifinite instances
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 20:45:10 +0100 |
huffman |
cleaned up instance proofs
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 20:35:52 +0100 |
huffman |
new-style instantiation proof for unit :: po
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 20:28:59 +0100 |
huffman |
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 20:04:40 +0100 |
huffman |
simplified chfin instance proof
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 05:15:43 +0100 |
huffman |
new compactness lemmas
|
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, 03 Jan 2008 22:10:52 +0100 |
huffman |
instance unit :: finite_po
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 18:29:03 +0100 |
huffman |
update instance proofs for sq_ord, po; new instance proofs for dcpo
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 00:53:30 +0100 |
huffman |
add constant unit_when
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 01:11:39 +0100 |
huffman |
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 01:02:29 +0100 |
huffman |
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
|
file |
diff |
annotate
|
| Wed, 12 Oct 2005 01:43:37 +0200 |
huffman |
added compactness lemmas; cleaned up
|
file |
diff |
annotate
|
| Tue, 11 Oct 2005 23:27:14 +0200 |
huffman |
added xsymbols syntax for pairs; cleaned up
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 05:30:02 +0200 |
huffman |
new syntax translations for continuous lambda abstraction
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 18:22:03 +0200 |
huffman |
add theorem cpair_defined_iff
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 02:37:42 +0200 |
huffman |
add lemma eq_cprod
|
file |
diff |
annotate
|