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-07 huffman 2010-10-07 remove some junk that made it in by accient
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-02 huffman 2010-10-02 minimize theory imports
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-03-22 huffman 2010-03-22 fix LaTeX overfull hbox warnings in HOLCF document
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-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-11-25 huffman 2008-11-25 renamed lemma compact_minimal to compact_bot_minimal; renamed compacts to approximants
2008-10-16 ballarin 2008-10-16 More occurrences of 'includes' gone.
2008-07-01 huffman 2008-07-01 rename compact_approx to compact_take
2008-07-01 huffman 2008-07-01 rename approx_pd to pd_take
2008-07-01 huffman 2008-07-01 split Completion.thy from CompactBasis.thy
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 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-19 huffman 2008-06-19 add lemmas take_chain_less and take_chain_le
2008-06-18 huffman 2008-06-18 replace preorder class with locale
2008-06-18 huffman 2008-06-18 add lemma compact_imp_principal to locale ideal_completion
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 remove commented text
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-02-02 huffman 2008-02-02 cleaned up
2008-01-18 huffman 2008-01-18 change lemma admD 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 new theory of powerdomains