src/HOLCF/IsaMakefile
2010-11-10 huffman 2010-11-10 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-10-19 huffman 2010-10-19 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
2010-10-16 huffman 2010-10-16 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
2010-10-11 huffman 2010-10-11 rename Ffun.thy to Fun_Cpo.thy
2010-10-11 huffman 2010-10-11 add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
2010-10-06 huffman 2010-10-06 major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);
2010-09-04 huffman 2010-09-04 add List_Cpo.thy to HOLCF/Library
2010-08-03 wenzelm 2010-08-03 renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
2010-07-12 wenzelm 2010-07-12 removed unused/untested IOA 'automaton' package;
2010-07-12 wenzelm 2010-07-12 removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
2010-05-25 wenzelm 2010-05-25 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;
2010-05-24 huffman 2010-05-24 move HOLCF/Sum_Cpo.thy to HOLCF/Library
2010-05-24 huffman 2010-05-24 move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
2010-05-24 huffman 2010-05-24 move unused pattern match syntax stuff into HOLCF/ex
2010-05-19 huffman 2010-05-19 move some example files into new HOLCF/Tutorial directory
2010-03-23 huffman 2010-03-23 move letrec stuff to new file HOLCF/ex/Letrec.thy
2010-03-22 huffman 2010-03-22 remove unused adm_tac.ML
2010-03-22 huffman 2010-03-22 remove obsolete holcf_logic.ML
2010-03-10 huffman 2010-03-10 adapt HOLCF to use Nat_Bijection library
2010-03-08 huffman 2010-03-08 move take-proofs stuff into new theory Domain_Aux.thy
2010-03-02 huffman 2010-03-02 update HOLCF makefile
2010-02-28 huffman 2010-02-28 move common functions into new file holcf_library.ML
2010-02-28 huffman 2010-02-28 move some powerdomain stuff into a new file
2010-02-18 huffman 2010-02-18 HOLCF-FOCUS depends on ex/Stream.thy
2010-02-17 huffman 2010-02-17 add theory HOLCF/ex/Strict_Fun.thy
2009-11-20 huffman 2009-11-20 example theory for new domain package
2009-11-19 huffman 2009-11-19 add dependency on domain_isomorphism.ML
2009-11-19 huffman 2009-11-19 add new makefile dependencies
2009-11-05 wenzelm 2009-11-05 more accurate cleanup;
2009-07-21 haftmann 2009-07-21 obey captialized directory names convention
2009-06-23 haftmann 2009-06-23 renamed ioa to automaton
2009-06-21 haftmann 2009-06-21 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-04-21 huffman 2009-04-21 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
2009-02-19 huffman 2009-02-19 add Powerdomain_ex.thy
2009-01-14 huffman 2009-01-14 rename Dsum.thy to Sum_Cpo.thy
2009-01-14 huffman 2009-01-14 change to simpler, more extensible continuity simproc define attribute [cont2cont] for continuity rules; new continuity simproc just applies cont2cont rules repeatedly; split theory Product_Cpo from Cprod, so Cfun can import Product_Cpo; add lemma cont2cont_LAM', which is suitable as a cont2cont rule.
2008-12-16 huffman 2008-12-16 new theory Dsum: cpo of disjoint sum
2008-10-04 wenzelm 2008-10-04 replaced ISATOOL by ISABELLE_TOOL;
2008-07-01 huffman 2008-07-01 put file dependencies on separate lines
2008-07-01 huffman 2008-07-01 add file dependencies
2008-06-30 huffman 2008-06-30 remove unused Cset.thy
2008-06-20 huffman 2008-06-20 replace SetPcpo.thy with Cset.thy
2008-03-28 wenzelm 2008-03-28 updated dependencies;
2007-10-23 nipkow 2007-10-23 changed back from ~=0 to >0
2007-05-31 wenzelm 2007-05-31 moved HOLCF tools to canonical place;
2007-04-26 wenzelm 2007-04-26 removed legacy ML files;
2006-09-28 wenzelm 2006-09-28 removed obsolete HOLCF.ML;
2006-06-02 wenzelm 2006-06-02 removed obsolete ML files;
2006-06-01 huffman 2006-06-01 removed legacy ML scripts
2006-05-28 wenzelm 2006-05-28 removed legacy ML scripts;
2006-05-28 wenzelm 2006-05-28 removed legacy ML scripts;
2006-05-27 wenzelm 2006-05-27 removed legacy ML scripts;
2006-05-27 wenzelm 2006-05-27 removed legacy ML scripts;
2006-05-27 wenzelm 2006-05-27 removed legacy ML scripts;
2006-05-03 huffman 2006-05-03 update to reflect changes in inverts/injects lemmas
2005-11-03 huffman 2005-11-03 removed ex/loeckx.ML
2005-10-19 wenzelm 2005-10-19 removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;
2005-09-03 wenzelm 2005-09-03 removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
2005-07-06 huffman 2005-07-06 add pcpodef files
2005-06-23 huffman 2005-06-23 add new file to test fixrec package