src/HOLCF/Adm.thy
2010-10-04 huffman 2010-10-04 new lemmas about lub
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
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-06-20 huffman 2008-06-20 tweak lemmas adm_all and adm_ball
2008-06-12 huffman 2008-06-12 remove unnecessary import of Ffun; add lemma admD2
2008-05-07 berghofe 2008-05-07 Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm, needs functions (since sets are now just functions).
2008-01-18 huffman 2008-01-18 change lemma admD to rule_format
2008-01-17 huffman 2008-01-17 convert lemma lub_mono to rule_format
2008-01-17 huffman 2008-01-17 rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
2008-01-17 huffman 2008-01-17 change class axiom chfin to rule_format
2008-01-14 huffman 2008-01-14 converted adm_all and adm_ball to rule_format; cleaned up
2008-01-10 huffman 2008-01-10 Compactness subsection with some new lemmas
2008-01-03 huffman 2008-01-03 remove legacy ML bindings
2008-01-03 huffman 2008-01-03 new lemma adm_upward
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-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2006-04-13 huffman 2006-04-13 add lemma less_UU_iff as default simp rule
2005-10-10 huffman 2005-10-10 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
2005-09-22 huffman 2005-09-22 added theorem adm_ball
2005-07-07 huffman 2005-07-07 use theorems ch2ch_cont, cont2contlubE
2005-07-01 huffman 2005-07-01 cleaned up; added adm_less to adm_lemmas; added subsection headings
2005-06-25 huffman 2005-06-25 cleaned up
2005-06-03 huffman 2005-06-03 changed to work with new contlubE rule
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 paulson 2005-05-24 cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
2005-05-24 huffman 2005-05-24 Moved admissibility definitions and lemmas to a separate theory