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