src/HOLCF/HOLCF.thy
2010-10-11 huffman 2010-10-11 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
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-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-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-03-22 huffman 2010-03-22 completely remove constants cpair, cfst, csnd
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-02-28 huffman 2010-02-28 move some powerdomain stuff into a new file
2009-11-10 huffman 2009-11-10 theory of representable cpos
2009-05-08 huffman 2009-05-08 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
2009-04-10 huffman 2009-04-10 set up domain package in Domain.thy
2009-03-20 wenzelm 2009-03-20 proper context for prove_cont/adm_tac;
2009-01-16 huffman 2009-01-16 merged
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.
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2009-01-05 wenzelm 2009-01-05 misc tuning and modernization;
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-12-16 huffman 2008-12-16 new theory Dsum: cpo of disjoint sum
2008-11-25 huffman 2008-11-25 add Algebraic and Universal to imports
2008-03-19 wenzelm 2008-03-19 eliminated change_claset/simpset;
2008-01-14 huffman 2008-01-14 new theory of powerdomains
2007-05-31 wenzelm 2007-05-31 moved HOLCF tools to canonical place;
2006-02-19 huffman 2006-02-19 use minimal imports
2005-10-19 wenzelm 2005-10-19 removed obsolete domain/interface.ML;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-09-23 wenzelm 2005-09-23 adm_tac/cont_tacRs: proper simpset;
2005-07-14 wenzelm 2005-07-14 use all files in HOLCF.thy;
2005-05-23 huffman 2005-05-23 moved continuity simproc to Cont.thy
2005-04-16 huffman 2005-04-16 speed improvements for the domain package
2005-04-02 huffman 2005-04-02 Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
2005-04-02 huffman 2005-04-02 converted to new-style theory
2005-03-04 huffman 2005-03-04 converted to new-style theories, and combined numbered files
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-03 wenzelm 2001-11-03 GPLed;
1997-05-25 slotosch 1997-05-25 Eliminated ccc1. Moved ID,oo into Cfun.
1997-03-26 nipkow 1997-03-26 Added "discrete" CPOs and modified IMP to use those rather than "lift"
1997-02-17 slotosch 1997-02-17 Changes of HOLCF from Oscar Slotosch: 1. axclass instead of class * less instead of less_fun, less_cfun, less_sprod, less_cprod, less_ssum, less_up, less_lift * @x.!y.x<<y instead of UUU instead of UU_fun, UU_cfun, ... * no witness type void needed (eliminated Void.thy.Void.ML) * inst_<typ>_<class> derived as theorems 2. improved some proves on less_sprod and less_cprod * eliminated the following theorems Sprod1.ML: less_sprod1a Sprod1.ML: less_sprod1b Sprod1.ML: less_sprod2a Sprod1.ML: less_sprod2b Sprod1.ML: less_sprod2c Sprod2.ML: less_sprod3a Sprod2.ML: less_sprod3b Sprod2.ML: less_sprod4b Sprod2.ML: less_sprod4c Sprod3.ML: less_sprod5b Sprod3.ML: less_sprod5c Cprod1.ML: less_cprod1b Cprod1.ML: less_cprod2a Cprod1.ML: less_cprod2b Cprod1.ML: less_cprod2c Cprod2.ML: less_cprod3a Cprod2.ML: less_cprod3b 3. new classes: * cpo<po, * chfin<pcpo, * flat<pcpo, * derived: flat<chfin to do: show instances for lift 4. Data Type One * Used lift for the definition: one = unit lift * Changed the constant one into ONE 5. Data Type Tr * Used lift for the definition: tr = bool lift * adopted definitions of if,andalso,orelse,neg * only one theory Tr.thy,Tr.ML instead of Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML * reintroduced ceils for =TT,=FF 6. typedef * Using typedef instead of faking type definitions to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun 7. adopted examples and domain construct to theses changes These changes eliminated all rules and arities from HOLCF
1996-12-09 sandnerr 1996-12-09 Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-10-06 regensbu 1995-10-06 added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.