src/HOLCF/IsaMakefile
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
2005-06-14 huffman 2005-06-14 moved continuity simproc to a separate file
2005-06-04 huffman 2005-06-04 added fixrec_package.ML
2005-06-04 huffman 2005-06-04 add Fixrec.thy
2005-06-03 huffman 2005-06-03 renamed FunCpo to Ffun
2005-05-24 paulson 2005-05-24 cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
2005-05-24 huffman 2005-05-24 New theory for defining subtypes of pcpos
2005-05-24 huffman 2005-05-24 Moved admissibility definitions and lemmas to a separate theory
2005-04-16 huffman 2005-04-16 speed improvements for the domain package
2005-03-07 huffman 2005-03-07 Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
2005-03-04 huffman 2005-03-04 converted to new-style theories, and combined numbered files
2005-03-02 huffman 2005-03-02 eliminated deps for removed files
2004-12-14 paulson 2004-12-14 tidied; removed references to HOL theories
2004-09-07 oheimb 2004-09-07 integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
2004-04-12 oheimb 2004-04-12 added Streams.thy (with stream concatenation etc.)
2001-12-27 wenzelm 2001-12-27 IMP/document/root.tex;
2001-12-09 kleing 2001-12-09 HOLCF/IMP converted to Isar
2001-11-03 wenzelm 2001-11-03 converted theory Dnat;
2001-11-03 wenzelm 2001-11-03 converted theory Lift;
2001-05-31 oheimb 2001-05-31 added FOCUS including the One-Element Buffer by Manfred Broy
2000-03-28 nipkow 2000-03-28 mods because of weak_case_cong -> removed Action.ML twice
1999-04-22 mueller 1999-04-22 added ex and Modelcheck
1999-02-03 wenzelm 1999-02-03 usedir -r;
1998-12-02 wenzelm 1998-12-02 tuned;
1998-12-02 wenzelm 1998-12-02 IOA-Storage: Memory storage case study.
1998-01-13 mueller 1998-01-13 added simulations files to IOA;
1998-01-12 mueller 1998-01-12 added further IOA liles;
1998-01-07 wenzelm 1998-01-07 improved targets; fixed dependencies on parent logics;
1997-12-19 wenzelm 1997-12-19 log files; 'clean' target;
1997-11-04 wenzelm 1997-11-04 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
1997-11-04 oheimb 1997-11-04 * removed "axioms" and "generated by" section * replaced "ops" section by extended "consts" section, which is capable of handling the continuous function space "->" directly * domain package: now uses normal mixfix annotations (instead of cinfix...)
1997-10-30 wenzelm 1997-10-30 added adm.ML;
1997-10-20 wenzelm 1997-10-20 removed Dlist;