| Sat, 27 Nov 2010 13:12:10 -0800 |
huffman |
renamed several HOLCF theorems (listed in NEWS)
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 11:42:35 -0800 |
huffman |
rename class 'bifinite' to 'domain'
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 15:47:46 -0700 |
huffman |
discontinue a bunch of legacy theorem names
|
file |
diff |
annotate
|
| Sat, 30 Oct 2010 15:13:11 -0700 |
huffman |
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 16:51:40 -0700 |
huffman |
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
|
file |
diff |
annotate
|
| Wed, 13 Oct 2010 10:56:42 -0700 |
huffman |
cleaned up Fun_Cpo.thy; deprecated a few theorem names
|
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
|
| Wed, 06 Oct 2010 10:49:27 -0700 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
file |
diff |
annotate
|
| Mon, 24 May 2010 12:42:17 -0700 |
huffman |
move HOLCF/Sum_Cpo.thy to HOLCF/Library
|
file |
diff |
annotate
|
| Mon, 24 May 2010 12:10:24 -0700 |
huffman |
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 23:34:23 -0700 |
huffman |
completely remove constants cpair, cfst, csnd
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 15:45:54 -0700 |
huffman |
remove unused adm_tac.ML
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 15:23:16 -0700 |
huffman |
remove obsolete holcf_logic.ML
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 14:55:42 -0800 |
huffman |
move some powerdomain stuff into a new file
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 06:22:29 -0800 |
huffman |
theory of representable cpos
|
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
|
| Fri, 10 Apr 2009 11:35:21 -0700 |
huffman |
set up domain package in Domain.thy
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 11:26:25 +0100 |
wenzelm |
proper context for prove_cont/adm_tac;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 13:07:44 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Wed, 14 Jan 2009 18:22:43 -0800 |
huffman |
rename Dsum.thy to Sum_Cpo.thy
|
file |
diff |
annotate
|
| Wed, 14 Jan 2009 17:11:29 -0800 |
huffman |
change to simpler, more extensible continuity simproc
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:56 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 18:13:26 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 09:44:59 -0800 |
huffman |
new theory Dsum: cpo of disjoint sum
|
file |
diff |
annotate
|
| Tue, 25 Nov 2008 23:29:26 +0100 |
huffman |
add Algebraic and Universal to imports
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:47:35 +0100 |
wenzelm |
eliminated change_claset/simpset;
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 19:26:41 +0100 |
huffman |
new theory of powerdomains
|
file |
diff |
annotate
|
| Thu, 31 May 2007 14:01:58 +0200 |
wenzelm |
moved HOLCF tools to canonical place;
|
file |
diff |
annotate
|