src/HOLCF/Bifinite.thy
2010-11-10 huffman 2010-11-10 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-11-10 huffman 2010-11-10 rename class 'bifinite' to 'domain'
2010-11-10 huffman 2010-11-10 add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
2010-11-10 huffman 2010-11-10 instance prod :: (predomain, predomain) predomain
2010-11-09 huffman 2010-11-09 add 'predomain' class: unpointed version of bifinite
2010-11-08 huffman 2010-11-08 reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
2010-10-21 huffman 2010-10-21 minimize imports
2010-10-14 huffman 2010-10-14 add type annotation to avoid warning
2010-10-11 huffman 2010-10-11 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
2010-10-11 huffman 2010-10-11 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
2010-10-09 huffman 2010-10-09 move all bifinite class instances to Bifinite.thy
2010-10-08 huffman 2010-10-08 rename class 'sfp' to 'bifinite'
2010-10-07 huffman 2010-10-07 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
2010-10-06 huffman 2010-10-06 major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);
2010-10-05 Brian Huffman 2010-10-05 add lemma finite_deflation_intro
2010-10-05 Brian Huffman 2010-10-05 add lemmas finite_deflation_imp_compact, cast_below_cast_iff
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-03-02 huffman 2010-03-02 proper names for types cfun, sprod, ssum
2009-11-19 huffman 2009-11-19 add map_ID lemmas
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-11 huffman 2009-05-11 move bifinite instance for product type from Cprod.thy to Bifinite.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-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-01-22 haftmann 2009-01-22 simplified handling of base sort, dropped axclass
2008-12-30 ballarin 2008-12-30 Merged.
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-09-16 ballarin 2008-09-16 Do not rely on locale assumption in interpretation.
2008-06-30 huffman 2008-06-30 reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
2008-06-20 huffman 2008-06-20 simplify profinite class axioms
2008-06-20 huffman 2008-06-20 clean up and rename some profinite lemmas
2008-06-12 huffman 2008-06-12 add lemma finite_image_approx; remove unnecessary sort annotations
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-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-14 huffman 2008-01-14 add class bifinite_cpo for possibly-unpointed bifinite domains
2008-01-14 huffman 2008-01-14 new theory of bifinite domains