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
|