src/HOLCF/Up.thy
2009-11-09 huffman 2009-11-09 add map_map lemmas
2009-11-05 huffman 2009-11-05 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
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-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-07-01 huffman 2008-07-01 remove unused lemma is_lub_Iup'
2008-07-01 huffman 2008-07-01 replace lub (range Y) with (LUB i. Y i)
2008-06-20 huffman 2008-06-20 simplify profinite class axioms
2008-05-19 huffman 2008-05-19 use new class package for classes profinite, bifinite; remove approx class
2008-03-26 huffman 2008-03-26 rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
2008-02-07 huffman 2008-02-07 fix broken syntax translations
2008-01-31 huffman 2008-01-31 add lemma cpo_lubI
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 added bifinite class instance
2008-01-14 huffman 2008-01-14 class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
2008-01-14 huffman 2008-01-14 compact_chfin is now declared simp
2008-01-10 huffman 2008-01-10 new compactness lemmas
2008-01-04 huffman 2008-01-04 new instance proofs for classes finite_po, chfin, flat
2008-01-02 huffman 2008-01-02 add dcpo instance proof
2008-01-02 huffman 2008-01-02 declare upE as cases rule; add new rule up_induct
2008-01-02 huffman 2008-01-02 update sq_ord/po instance proofs
2008-01-02 huffman 2008-01-02 remove not_up_less_UU [simp]
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2006-02-19 huffman 2006-02-19 use minimal imports
2005-11-30 huffman 2005-11-30 add xsymbol syntax for u type constructor
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-10-12 huffman 2005-10-12 added compactness theorems
2005-09-22 huffman 2005-09-22 cleaned up
2005-07-28 wenzelm 2005-07-28 fixed var index in tactic;
2005-07-08 huffman 2005-07-08 define 'a u with datatype package; removed obsolete lemmas; renamed upE1 to upE and Exh_Up1 to Exh_Up; cleaned up
2005-06-23 huffman 2005-06-23 add csplit3, ssplit3, fup3 as simp rules
2005-06-08 huffman 2005-06-08 make up_eq and up_less into simp rules
2005-06-08 huffman 2005-06-08 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
2005-06-03 huffman 2005-06-03 changed to use new contlubI, etc.
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-03-10 huffman 2005-03-10 instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
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