src/HOLCF/Cfun.thy
2010-11-10 huffman 2010-11-10 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-11-03 huffman 2010-11-03 remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
2010-10-29 huffman 2010-10-29 renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
2010-10-29 huffman 2010-10-29 renamed lemma cont2cont_Rep_CFun to cont2cont_APP
2010-10-22 huffman 2010-10-22 add lemma strict3
2010-10-22 huffman 2010-10-22 make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
2010-10-22 huffman 2010-10-22 remove finite_po class
2010-10-20 huffman 2010-10-20 introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
2010-10-13 huffman 2010-10-13 cleaned up Fun_Cpo.thy; deprecated a few theorem names
2010-10-12 huffman 2010-10-12 move lemmas from Lift.thy to Cfun.thy
2010-10-12 huffman 2010-10-12 remove unneeded lemmas from Fun_Cpo.thy
2010-10-12 huffman 2010-10-12 remove unused lemmas
2010-10-12 huffman 2010-10-12 remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2
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-11 huffman 2010-10-11 rename Ffun.thy to Fun_Cpo.thy
2010-10-07 huffman 2010-10-07 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
2010-09-30 huffman 2010-09-30 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 renamed expand_*_eq in HOLCF as well
2010-09-04 huffman 2010-09-04 add lemma cont2cont_Let_simple
2010-05-22 huffman 2010-05-22 add beta_cfun simproc, which uses cont2cont rules
2010-05-22 huffman 2010-05-22 remove cont2cont simproc; instead declare cont2cont rules as simp rules
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-03-23 huffman 2010-03-23 remove continuous let-binding function CLet; add cont2cont rule ordinary Let
2010-03-22 huffman 2010-03-22 remove contlub predicate
2010-03-14 huffman 2010-03-14 use headers consistently
2010-03-07 huffman 2010-03-07 add simp rule LAM_strict
2010-03-03 wenzelm 2010-03-03 merged, resolving some basic conflicts;
2010-03-02 huffman 2010-03-02 proper names for types cfun, sprod, ssum
2010-03-02 wenzelm 2010-03-02 proper (type_)notation;
2010-02-17 huffman 2010-02-17 fix warnings about duplicate simp rules
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
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-05-06 huffman 2009-05-06 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
2009-01-14 huffman 2009-01-14 minimize dependencies
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 remove cvs Id tags
2008-12-11 wenzelm 2008-12-11 pcpodef package: state two goals, instead of encoded conjunction;
2008-12-10 huffman 2008-12-10 cleaned up some proofs in Cfun.thy
2008-07-01 huffman 2008-07-01 replace lub (range Y) with (LUB i. Y i)
2008-06-19 huffman 2008-06-19 add lemma cfcomp_LAM
2008-01-31 huffman 2008-01-31 instances for class discrete_cpo
2008-01-18 huffman 2008-01-18 add space to binder syntax
2008-01-17 huffman 2008-01-17 change class axiom chfin to rule_format
2008-01-16 huffman 2008-01-16 change class axiom ax_flat to rule_format
2008-01-14 huffman 2008-01-14 added lemmas lub_distribs
2008-01-10 huffman 2008-01-10 declare ch2ch_LAM [simp]
2008-01-04 huffman 2008-01-04 new instance proofs for classes finite_po, chfin, flat
2008-01-02 huffman 2008-01-02 move lemmas from Cont.thy to Ffun.thy; reorder dependency of Cont.thy and Ffun.thy; add dcpo instance proofs for function type
2007-12-20 huffman 2007-12-20 move bottom-related stuff back into Pcpo.thy
2007-12-18 huffman 2007-12-18 add class ppo of pointed partial orders; define UU in class ppo instead of pcpo; add new lemmas about lub
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'axiomatization');
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2007-05-31 wenzelm 2007-05-31 moved HOLCF tools to canonical place;
2006-05-24 huffman 2006-05-24 add theorem cfcomp_strict
2005-11-05 huffman 2005-11-05 renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-11-05 huffman 2005-11-05 add line breaks to Rep_CFun syntax
2005-11-04 huffman 2005-11-04 moved adm_chfindom from Fix.thy to Cfun.thy
2005-11-04 huffman 2005-11-04 add print translation: Abs_CFun f => LAM x. f x
2005-11-03 huffman 2005-11-03 add translation for wildcard pattern