| Fri, 29 Oct 2010 17:15:28 -0700 |
huffman |
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
|
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
|
| 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
|
| Fri, 08 Oct 2010 07:39:50 -0700 |
huffman |
rename class 'sfp' to 'bifinite'
|
file |
diff |
annotate
|
| Thu, 07 Oct 2010 13:33:06 -0700 |
huffman |
add lemma typedef_ideal_completion
|
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:07:57 -0700 |
Brian Huffman |
simplify proofs of powerdomain inequalities
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 11:39:27 +0200 |
haftmann |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 13:27:35 -0700 |
huffman |
fix LaTeX overfull hbox warnings in HOLCF document
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:43 +0100 |
haftmann |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 21:44:37 -0800 |
huffman |
add map_ID lemmas
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 12:40:47 -0800 |
huffman |
ep_pair and deflation lemmas for powerdomain map functions
|
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, 19 Feb 2009 06:47:06 -0800 |
huffman |
avoid using ab_semigroup_idem_mult locale for powerdomains
|
file |
diff |
annotate
|
| Thu, 29 Jan 2009 10:07:43 +0100 |
nipkow |
commented out unused lemmas. May need to be put back by Brian.
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:56 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Fri, 19 Dec 2008 11:57:21 +0100 |
ballarin |
More porting to new locales.
|
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, 01 Jul 2008 00:58:19 +0200 |
huffman |
rename approx_pd to pd_take
|
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 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
|
| 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
|
| Wed, 18 Jun 2008 23:03:11 +0200 |
huffman |
add lemma compact_imp_principal to locale ideal_completion
|
file |
diff |
annotate
|