src/HOLCF/Fix.thy
2010-10-12 huffman 2010-10-12 reformulate lemma cont2cont_lub and move to Cont.thy
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-04-06 krauss 2010-04-06 tuned proof (no induction needed); removed unused lemma and fuzzy comment
2010-03-23 huffman 2010-03-23 minimize dependencies
2010-03-23 huffman 2010-03-23 move letrec stuff to new file HOLCF/ex/Letrec.thy
2010-03-22 huffman 2010-03-22 define CLetrec using Pair, fst, snd instead of cpair, cfst, csnd
2010-03-22 huffman 2010-03-22 convert lemma fix_cprod to use Pair, fst, snd
2010-03-22 huffman 2010-03-22 remove admw predicate
2010-03-14 huffman 2010-03-14 use headers consistently
2010-02-07 huffman 2010-02-07 add lemma iterate_below_fix
2010-01-16 haftmann 2010-01-16 dropped some old primrecs and some constdefs
2009-11-10 huffman 2009-11-10 add lemma parallel_fix_ind
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
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-06-22 huffman 2008-06-22 use new-style abbreviation/notation for fix syntax
2008-06-19 huffman 2008-06-19 add lemma iterate_iterate
2008-06-12 huffman 2008-06-12 change orientation of fix_eqI and convert to rule_format; add lemma fix_ind2
2008-01-18 huffman 2008-01-18 add space to binder syntax
2008-01-18 huffman 2008-01-18 change lemma admD to rule_format
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2005-11-06 huffman 2005-11-06 add proof of Bekic's theorem: fix_cprod
2005-11-05 huffman 2005-11-05 put iterate and fix in separate sections; added Letrec
2005-11-05 huffman 2005-11-05 renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-11-04 huffman 2005-11-04 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
2005-11-03 huffman 2005-11-03 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
2005-11-03 huffman 2005-11-03 reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
2005-10-10 huffman 2005-10-10 new syntax translations for continuous lambda abstraction
2005-09-22 huffman 2005-09-22 cleaned up
2005-07-26 huffman 2005-07-26 add theorem fix_defined_iff; cleaned up
2005-06-23 huffman 2005-06-23 added theorems fix_strict, fix_defined, fix_id, fix_const
2005-06-14 huffman 2005-06-14 renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
2005-06-03 huffman 2005-06-03 cleaned up proof of cont_Ifix
2005-05-26 huffman 2005-05-26 added defaultsort declaration
2005-05-26 huffman 2005-05-26 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-05-24 huffman 2005-05-24 Moved admissibility definitions and lemmas to a separate theory
2005-05-18 huffman 2005-05-18 shortened proof of adm_disj
2005-05-18 huffman 2005-05-18 cleaned up and shortened some proofs
2005-04-27 huffman 2005-04-27 Added binder syntax for fix
2005-03-31 huffman 2005-03-31 changed comments to text blocks, cleaned up a few proofs
2005-03-04 huffman 2005-03-04 fix headers
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;
2001-01-09 nipkow 2001-01-09 *** empty log message ***
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-03-10 oheimb 1998-03-10 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-25 slotosch 1997-05-25 Moved the classes flat chfin from Fix to Pcpo. Corresponding theorems from Fix into Pcpo,Cont,Cfun3
1997-05-25 slotosch 1997-05-25 Eliminated the prediates flat,chfin Changed theorems with flat(x::'a) to (x::'a::flat) Since flat<chfin theorems adm_flat,adm_flatdom are eliminated. Use adm_chain_finite and adm_chfindom instead! Examples do not use flat_flat any more
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-11-29 oheimb 1996-11-29 renamed is_flat to flat, moved Lift*.* to Up*.*, renaming of all constans and theorems concerned, (*lift* to *up*, except Ilift to Ifup, lift to fup)
1996-09-12 oheimb 1996-09-12 added comment on is_flat
1996-06-25 berghofe 1996-06-25 Changed argument order of nat_rec.
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-12-20 regensbu 1995-12-20 changed predicate flat to is_flat in theory Fix.thy
1995-06-29 regensbu 1995-06-29 The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported
1995-06-21 clasohm 1995-06-21 removed \...\ inside strings
1994-06-29 clasohm 1994-06-29 added parentheses made necessary by change of constrain's precedence