src/HOLCF/ConvexPD.thy
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-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-11-05 huffman 2010-11-05 (infixl "<<" 55) -> (infix "<<" 50)
2010-11-03 huffman 2010-11-03 remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
2010-10-29 huffman 2010-10-29 renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
2010-10-27 huffman 2010-10-27 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
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-08 huffman 2010-10-08 rename class 'sfp' to 'bifinite'
2010-10-07 huffman 2010-10-07 add lemma typedef_ideal_completion
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 simplify proofs of powerdomain inequalities
2010-07-12 haftmann 2010-07-12 avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-03-22 huffman 2010-03-22 fix LaTeX overfull hbox warnings in HOLCF document
2010-01-28 haftmann 2010-01-28 dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2009-11-19 huffman 2009-11-19 add map_ID lemmas
2009-11-09 huffman 2009-11-09 ep_pair and deflation lemmas for powerdomain map functions
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-02-19 huffman 2009-02-19 avoid using ab_semigroup_idem_mult locale for powerdomains
2009-01-29 nipkow 2009-01-29 commented out unused lemmas. May need to be put back by Brian.
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2008-12-30 ballarin 2008-12-30 Merged.
2008-12-19 ballarin 2008-12-19 More porting to new locales.
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-07-01 huffman 2008-07-01 rename approx_pd to pd_take
2008-06-26 huffman 2008-06-26 remove cset theory; define ideal completions using typedef instead of cpodef
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-20 huffman 2008-06-20 removed SetPcpo.thy and cpo instance for type bool; added Cset.thy with pcpo type 'a cset isomorphic to 'a set; updated ideal completion theory to use cset
2008-06-19 huffman 2008-06-19 move lemmas into locales; restructure some proofs
2008-06-18 huffman 2008-06-18 add lemma compact_imp_principal to locale ideal_completion
2008-05-19 huffman 2008-05-19 use new class package for classes profinite, bifinite; remove approx class
2008-05-16 huffman 2008-05-16 rename locales; add completion_approx constant to ideal_completion locale; add new set-like syntax for powerdomains; reorganized proofs
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-03-27 huffman 2008-03-27 make preorder locale into a superclass of class po
2008-03-26 huffman 2008-03-26 rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
2008-02-06 haftmann 2008-02-06 locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
2008-01-18 huffman 2008-01-18 change lemma admD to rule_format
2008-01-14 huffman 2008-01-14 new theory of powerdomains