| 2010-11-11 |
huffman |
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
|
file |
diff |
annotate
|
| 2010-10-19 |
huffman |
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
|
file |
diff |
annotate
|
| 2010-10-16 |
huffman |
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
|
file |
diff |
annotate
|
| 2010-10-11 |
huffman |
rename Ffun.thy to Fun_Cpo.thy
|
file |
diff |
annotate
|
| 2010-10-11 |
huffman |
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
|
file |
diff |
annotate
|
| 2010-10-06 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
file |
diff |
annotate
|
| 2010-09-04 |
huffman |
add List_Cpo.thy to HOLCF/Library
|
file |
diff |
annotate
|
| 2010-08-03 |
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
|
| 2010-07-12 |
wenzelm |
removed unused/untested IOA 'automaton' package;
|
file |
diff |
annotate
|
| 2010-07-12 |
wenzelm |
removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
|
file |
diff |
annotate
|
| 2010-05-25 |
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
|
| 2010-05-24 |
huffman |
move HOLCF/Sum_Cpo.thy to HOLCF/Library
|
file |
diff |
annotate
|
| 2010-05-24 |
huffman |
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
|
file |
diff |
annotate
|
| 2010-05-24 |
huffman |
move unused pattern match syntax stuff into HOLCF/ex
|
file |
diff |
annotate
|
| 2010-05-20 |
huffman |
move some example files into new HOLCF/Tutorial directory
|
file |
diff |
annotate
|
| 2010-03-23 |
huffman |
move letrec stuff to new file HOLCF/ex/Letrec.thy
|
file |
diff |
annotate
|
| 2010-03-22 |
huffman |
remove unused adm_tac.ML
|
file |
diff |
annotate
|
| 2010-03-22 |
huffman |
remove obsolete holcf_logic.ML
|
file |
diff |
annotate
|
| 2010-03-10 |
huffman |
adapt HOLCF to use Nat_Bijection library
|
file |
diff |
annotate
|
| 2010-03-08 |
huffman |
move take-proofs stuff into new theory Domain_Aux.thy
|
file |
diff |
annotate
|
| 2010-03-03 |
huffman |
update HOLCF makefile
|
file |
diff |
annotate
|
| 2010-02-28 |
huffman |
move common functions into new file holcf_library.ML
|
file |
diff |
annotate
|
| 2010-02-28 |
huffman |
move some powerdomain stuff into a new file
|
file |
diff |
annotate
|
| 2010-02-18 |
huffman |
HOLCF-FOCUS depends on ex/Stream.thy
|
file |
diff |
annotate
|
| 2010-02-17 |
huffman |
add theory HOLCF/ex/Strict_Fun.thy
|
file |
diff |
annotate
|
| 2009-11-20 |
huffman |
example theory for new domain package
|
file |
diff |
annotate
|
| 2009-11-19 |
huffman |
add dependency on domain_isomorphism.ML
|
file |
diff |
annotate
|
| 2009-11-19 |
huffman |
add new makefile dependencies
|
file |
diff |
annotate
|
| 2009-11-05 |
wenzelm |
more accurate cleanup;
|
file |
diff |
annotate
|
| 2009-07-21 |
haftmann |
obey captialized directory names convention
|
file |
diff |
annotate
|
| 2009-06-23 |
haftmann |
renamed ioa to automaton
|
file |
diff |
annotate
|
| 2009-06-21 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| 2009-04-22 |
huffman |
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
|
file |
diff |
annotate
|
| 2009-02-19 |
huffman |
add Powerdomain_ex.thy
|
file |
diff |
annotate
|
| 2009-01-15 |
huffman |
rename Dsum.thy to Sum_Cpo.thy
|
file |
diff |
annotate
|
| 2009-01-15 |
huffman |
change to simpler, more extensible continuity simproc
|
file |
diff |
annotate
|
| 2008-12-16 |
huffman |
new theory Dsum: cpo of disjoint sum
|
file |
diff |
annotate
|
| 2008-10-04 |
wenzelm |
replaced ISATOOL by ISABELLE_TOOL;
|
file |
diff |
annotate
|
| 2008-07-01 |
huffman |
put file dependencies on separate lines
|
file |
diff |
annotate
|
| 2008-06-30 |
huffman |
add file dependencies
|
file |
diff |
annotate
|
| 2008-06-30 |
huffman |
remove unused Cset.thy
|
file |
diff |
annotate
|
| 2008-06-20 |
huffman |
replace SetPcpo.thy with Cset.thy
|
file |
diff |
annotate
|
| 2008-03-27 |
wenzelm |
updated dependencies;
|
file |
diff |
annotate
|
| 2007-10-23 |
nipkow |
changed back from ~=0 to >0
|
file |
diff |
annotate
|
| 2007-05-31 |
wenzelm |
moved HOLCF tools to canonical place;
|
file |
diff |
annotate
|
| 2007-04-26 |
wenzelm |
removed legacy ML files;
|
file |
diff |
annotate
|
| 2006-09-28 |
wenzelm |
removed obsolete HOLCF.ML;
|
file |
diff |
annotate
|
| 2006-06-02 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| 2006-06-01 |
huffman |
removed legacy ML scripts
|
file |
diff |
annotate
|
| 2006-05-28 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| 2006-05-28 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| 2006-05-27 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| 2006-05-27 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| 2006-05-27 |
wenzelm |
removed legacy ML scripts;
|
file |
diff |
annotate
|
| 2006-05-03 |
huffman |
update to reflect changes in inverts/injects lemmas
|
file |
diff |
annotate
|
| 2005-11-02 |
huffman |
removed ex/loeckx.ML
|
file |
diff |
annotate
|
| 2005-10-19 |
wenzelm |
removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;
|
file |
diff |
annotate
|
| 2005-09-03 |
wenzelm |
removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
|
file |
diff |
annotate
|
| 2005-07-05 |
huffman |
add pcpodef files
|
file |
diff |
annotate
|
| 2005-06-23 |
huffman |
add new file to test fixrec package
|
file |
diff |
annotate
|