| Sat, 27 Nov 2010 14:09:03 -0800 |
huffman |
rename Pcpodef.thy to Cpodef.thy;
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 08:47:58 -0800 |
huffman |
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 11:50:05 -0800 |
huffman |
rename 'repdef' to 'domaindef'
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 18:30:17 -0800 |
huffman |
merge Representable.thy into Domain.thy
|
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
|
| Tue, 19 Oct 2010 15:01:51 -0700 |
huffman |
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
|
file |
diff |
annotate
|
| Sat, 16 Oct 2010 16:22:42 -0700 |
huffman |
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 16:24:44 -0700 |
huffman |
rename Ffun.thy to Fun_Cpo.thy
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 09:54:04 -0700 |
huffman |
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 10:49:27 -0700 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 07:26:34 -0700 |
huffman |
add List_Cpo.thy to HOLCF/Library
|
file |
diff |
annotate
|
| Tue, 03 Aug 2010 16:57:45 +0200 |
wenzelm |
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 22:35:41 +0200 |
wenzelm |
removed unused/untested IOA 'automaton' package;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 20:35:10 +0200 |
wenzelm |
removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
|
file |
diff |
annotate
|
| Tue, 25 May 2010 22:12:26 +0200 |
wenzelm |
renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;
|
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
|
| Mon, 24 May 2010 11:29:49 -0700 |
huffman |
move unused pattern match syntax stuff into HOLCF/ex
|
file |
diff |
annotate
|
| Wed, 19 May 2010 17:01:07 -0700 |
huffman |
move some example files into new HOLCF/Tutorial directory
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 09:39:21 -0700 |
huffman |
move letrec stuff to new file HOLCF/ex/Letrec.thy
|
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
|
| Wed, 10 Mar 2010 15:20:13 -0800 |
huffman |
adapt HOLCF to use Nat_Bijection library
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 08:12:48 -0800 |
huffman |
move take-proofs stuff into new theory Domain_Aux.thy
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 20:16:35 -0800 |
huffman |
update HOLCF makefile
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 15:30:44 -0800 |
huffman |
move common functions into new file holcf_library.ML
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 14:55:42 -0800 |
huffman |
move some powerdomain stuff into a new file
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 12:36:09 -0800 |
huffman |
HOLCF-FOCUS depends on ex/Stream.thy
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 08:05:16 -0800 |
huffman |
add theory HOLCF/ex/Strict_Fun.thy
|
file |
diff |
annotate
|
| Fri, 20 Nov 2009 00:06:04 -0800 |
huffman |
example theory for new domain package
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 12:38:25 -0800 |
huffman |
add dependency on domain_isomorphism.ML
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:08:57 -0800 |
huffman |
add new makefile dependencies
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 16:23:51 +0100 |
wenzelm |
more accurate cleanup;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 16:14:56 +0200 |
haftmann |
obey captialized directory names convention
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:08:35 +0200 |
haftmann |
renamed ioa to automaton
|
file |
diff |
annotate
|
| Sun, 21 Jun 2009 08:38:58 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Tue, 21 Apr 2009 17:01:45 -0700 |
huffman |
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 09:39:49 -0800 |
huffman |
add Powerdomain_ex.thy
|
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
|
| Tue, 16 Dec 2008 09:44:59 -0800 |
huffman |
new theory Dsum: cpo of disjoint sum
|
file |
diff |
annotate
|
| Sat, 04 Oct 2008 16:05:09 +0200 |
wenzelm |
replaced ISATOOL by ISABELLE_TOOL;
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 07:13:45 +0200 |
huffman |
put file dependencies on separate lines
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 01:28:44 +0200 |
huffman |
add file dependencies
|
file |
diff |
annotate
|
| Mon, 30 Jun 2008 21:47:56 +0200 |
huffman |
remove unused Cset.thy
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 22:28:10 +0200 |
huffman |
replace SetPcpo.thy with Cset.thy
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 00:02:56 +0100 |
wenzelm |
updated dependencies;
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 22:48:25 +0200 |
nipkow |
changed back from ~=0 to >0
|
file |
diff |
annotate
|
| Thu, 31 May 2007 14:01:58 +0200 |
wenzelm |
moved HOLCF tools to canonical place;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 16:39:31 +0200 |
wenzelm |
removed legacy ML files;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:53 +0200 |
wenzelm |
removed obsolete HOLCF.ML;
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 20:12:59 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Thu, 01 Jun 2006 23:53:29 +0200 |
huffman |
removed legacy ML scripts
|
file |
diff |
annotate
|
| Sun, 28 May 2006 20:53:03 +0200 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| Sun, 28 May 2006 19:54:20 +0200 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 21:18:51 +0200 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 21:00:31 +0200 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 19:49:36 +0200 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| Wed, 03 May 2006 03:47:15 +0200 |
huffman |
update to reflect changes in inverts/injects lemmas
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 00:32:47 +0100 |
huffman |
removed ex/loeckx.ML
|
file |
diff |
annotate
|