| 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
|
| Sun, 19 Feb 2006 02:11:27 +0100 |
huffman |
use minimal imports
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 21:52:35 +0200 |
wenzelm |
removed obsolete domain/interface.ML;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:13 +0200 |
wenzelm |
change_claset/simpset;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:21:52 +0200 |
wenzelm |
adm_tac/cont_tacRs: proper simpset;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:23 +0200 |
wenzelm |
use all files in HOLCF.thy;
|
file |
diff |
annotate
|
| Mon, 23 May 2005 23:24:38 +0200 |
huffman |
moved continuity simproc to Cont.thy
|
file |
diff |
annotate
|
| Sat, 16 Apr 2005 00:17:52 +0200 |
huffman |
speed improvements for the domain package
|
file |
diff |
annotate
|
| Sat, 02 Apr 2005 00:33:51 +0200 |
huffman |
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
|
file |
diff |
annotate
|
| Sat, 02 Apr 2005 00:12:38 +0200 |
huffman |
converted to new-style theory
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 23:12:36 +0100 |
huffman |
converted to new-style theories, and combined numbered files
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:41:26 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Sun, 25 May 1997 18:45:25 +0200 |
slotosch |
Eliminated ccc1. Moved ID,oo into Cfun.
|
file |
diff |
annotate
|
| Wed, 26 Mar 1997 17:58:48 +0100 |
nipkow |
Added "discrete" CPOs and modified IMP to use those rather than "lift"
|
file |
diff |
annotate
|
| Mon, 17 Feb 1997 10:57:11 +0100 |
slotosch |
Changes of HOLCF from Oscar Slotosch:
|
file |
diff |
annotate
|
| Mon, 09 Dec 1996 19:16:20 +0100 |
sandnerr |
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
|
file |
diff |
annotate
|
| Tue, 06 Feb 1996 12:42:31 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 06 Oct 1995 17:25:24 +0100 |
regensbu |
added 8bit pragmas
|
file |
diff |
annotate
|
| Wed, 19 Jan 1994 17:35:01 +0100 |
nipkow |
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
|
file |
diff |
annotate
|