src/HOLCF/Cfun.thy
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
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 cleaned up; ch2ch_Rep_CFun is a simp rule
2005-10-11 huffman 2005-10-11 rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less
2005-10-10 huffman 2005-10-10 add names to infix declarations
2005-10-10 huffman 2005-10-10 new syntax translations for continuous lambda abstraction
2005-10-10 huffman 2005-10-10 removed Istrictify; simplified some proofs
2005-07-26 huffman 2005-07-26 cleaned up
2005-07-06 huffman 2005-07-06 use new pcpodef package
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-06-14 huffman 2005-06-14 moved continuity simproc to a separate file
2005-06-08 huffman 2005-06-08 added theorem injection_less
2005-06-03 huffman 2005-06-03 removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
2005-05-27 huffman 2005-05-27 use TypedefPcpo for all class instances
2005-05-27 huffman 2005-05-27 Use TypedefPcpo theorem for po instance
2005-05-27 huffman 2005-05-27 use thelub_const lemma
2005-05-26 huffman 2005-05-26 rewrote continuous isomorphism section, cleaned up
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-05-23 huffman 2005-05-23 moved continuity simproc to Cfun.thy
2005-03-31 huffman 2005-03-31 added theorems eta_cfun and cont2cont_eta
2005-03-10 huffman 2005-03-10 fixed filename in header
2005-03-08 huffman 2005-03-08 reordered and arranged for document generation, cleaned up some 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