| Tue, 25 Nov 2008 23:28:06 +0100 |
huffman |
renamed lemma compact_minimal to compact_bot_minimal;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 17:19:47 +0200 |
ballarin |
More occurrences of 'includes' gone.
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 01:09:03 +0200 |
huffman |
rename compact_approx to compact_take
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 00:58:19 +0200 |
huffman |
rename approx_pd to pd_take
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 00:52:46 +0200 |
huffman |
split Completion.thy from CompactBasis.thy
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 17:54:05 +0200 |
huffman |
remove cset theory; define ideal completions using typedef instead of cpodef
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 22:51:50 +0200 |
huffman |
clean up and rename some profinite lemmas
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 20:03:13 +0200 |
huffman |
removed SetPcpo.thy and cpo instance for type bool;
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 22:50:58 +0200 |
huffman |
move lemmas into locales;
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 22:43:59 +0200 |
huffman |
add lemmas take_chain_less and take_chain_le
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 23:07:30 +0200 |
huffman |
replace preorder class with locale
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 23:03:11 +0200 |
huffman |
add lemma compact_imp_principal to locale ideal_completion
|
file |
diff |
annotate
|
| Fri, 16 May 2008 23:25:37 +0200 |
huffman |
rename locales;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:57:19 +0200 |
berghofe |
Adapted to encoding of sets as predicates
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 21:49:10 +0100 |
huffman |
remove commented text
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 00:27:16 +0100 |
huffman |
make preorder locale into a superclass of class po
|
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
|
| Wed, 06 Feb 2008 08:34:32 +0100 |
haftmann |
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
|
file |
diff |
annotate
|
| Sat, 02 Feb 2008 03:26:40 +0100 |
huffman |
cleaned up
|
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 21:44:19 +0100 |
huffman |
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 19:26:41 +0100 |
huffman |
new theory of powerdomains
|
file |
diff |
annotate
|