src/HOLCF/Powerdomains.thy
2010-11-26 huffman 2010-11-26 remove map function names from domain package theory data
2010-11-08 huffman 2010-11-08 implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
2010-10-27 huffman 2010-10-27 make domain package work with non-cpo argument types
2010-10-26 huffman 2010-10-26 use Named_Thms instead of Theory_Data for some domain package theorems
2010-10-11 huffman 2010-10-11 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
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-02-28 huffman 2010-02-28 store deflation thms for map functions in theory data
2010-02-28 huffman 2010-02-28 move some powerdomain stuff into a new file