src/HOLCF/CompactBasis.thy
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