src/HOLCF/Cfun.thy
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