| 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
|