src/HOLCF/Ffun.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
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-07-01 huffman 2008-07-01 range_composition no longer in simp set
2008-07-01 huffman 2008-07-01 replace lub (range Y) with (LUB i. Y i)
2008-03-27 huffman 2008-03-27 declare cont_lemmas_ext as simp rules individually
2008-01-31 huffman 2008-01-31 add lemma is_lub_lambda
2008-01-31 huffman 2008-01-31 instances for class discrete_cpo
2008-01-17 huffman 2008-01-17 convert lemma lub_mono to rule_format
2008-01-17 huffman 2008-01-17 change class axiom chfin to rule_format
2008-01-14 huffman 2008-01-14 class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
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
2008-01-02 huffman 2008-01-02 update instance proofs to new style
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2005-11-30 huffman 2005-11-30 changed section names
2005-11-05 huffman 2005-11-05 renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-10-11 huffman 2005-10-11 cleaned up; renamed less_fun to expand_fun_less
2005-06-03 huffman 2005-06-03 renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict