| Wed, 17 Nov 2010 08:47:58 -0800 |
huffman |
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 18:45:48 -0800 |
huffman |
section headings
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 17:56:08 -0800 |
huffman |
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 11:42:35 -0800 |
huffman |
rename class 'bifinite' to 'domain'
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 08:18:32 -0800 |
huffman |
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 06:02:37 -0800 |
huffman |
instance prod :: (predomain, predomain) predomain
|
file |
diff |
annotate
|
| Tue, 09 Nov 2010 16:37:13 -0800 |
huffman |
add 'predomain' class: unpointed version of bifinite
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 06:58:09 -0800 |
huffman |
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 15:21:39 -0700 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Thu, 14 Oct 2010 09:28:05 -0700 |
huffman |
add type annotation to avoid warning
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 21:35:31 -0700 |
huffman |
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 08:32:09 -0700 |
huffman |
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
|
file |
diff |
annotate
|
| Sat, 09 Oct 2010 07:24:49 -0700 |
huffman |
move all bifinite class instances to Bifinite.thy
|
file |
diff |
annotate
|
| Fri, 08 Oct 2010 07:39:50 -0700 |
huffman |
rename class 'sfp' to 'bifinite'
|
file |
diff |
annotate
|
| Thu, 07 Oct 2010 13:54:43 -0700 |
huffman |
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 10:49:27 -0700 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 17:53:00 -0700 |
Brian Huffman |
add lemma finite_deflation_intro
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 17:36:45 -0700 |
Brian Huffman |
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 17:21:10 -0800 |
huffman |
proper names for types cfun, sprod, ssum
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 21:44:37 -0800 |
huffman |
add map_ID lemmas
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 15:51:32 -0800 |
huffman |
add map_map lemmas
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 11:47:00 -0800 |
huffman |
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
|
file |
diff |
annotate
|
| Mon, 11 May 2009 12:26:33 -0700 |
huffman |
move bifinite instance for product type from Cprod.thy to Bifinite.thy
|
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
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Thu, 22 Jan 2009 09:04:46 +0100 |
haftmann |
simplified handling of base sort, dropped axclass
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 12:25:26 +0200 |
ballarin |
Do not rely on locale assumption in interpretation.
|
file |
diff |
annotate
|
| Mon, 30 Jun 2008 22:16:47 +0200 |
huffman |
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 23:01:09 +0200 |
huffman |
simplify profinite class axioms
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 22:51:50 +0200 |
huffman |
clean up and rename some profinite lemmas
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 22:41:03 +0200 |
huffman |
add lemma finite_image_approx; remove unnecessary sort annotations
|
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
|
| Thu, 17 Jan 2008 21:56:33 +0100 |
huffman |
convert lemma lub_mono 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 21:15:20 +0100 |
huffman |
add class bifinite_cpo for possibly-unpointed bifinite domains
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 19:26:01 +0100 |
huffman |
new theory of bifinite domains
|
file |
diff |
annotate
|