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-10 huffman 2010-11-10 instance prod :: (predomain, predomain) predomain
2010-11-09 huffman 2010-11-09 add 'predomain' class: unpointed version of bifinite
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-19 huffman 2010-10-19 replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
2010-10-19 huffman 2010-10-19 eliminate constant 'coerce'; use 'prj oo emb' instead
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-09 huffman 2010-10-09 move all bifinite class instances to Bifinite.thy
2010-10-08 huffman 2010-10-08 rename class 'sfp' to 'bifinite'
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-07-12 haftmann 2010-07-12 avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
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
2010-03-22 huffman 2010-03-22 remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2010-03-08 huffman 2010-03-08 move take-proofs stuff into new theory Domain_Aux.thy
2010-03-05 huffman 2010-03-05 add comment
2010-03-05 huffman 2010-03-05 move take_proofs-related stuff to a new section
2010-03-03 huffman 2010-03-03 merged
2010-03-03 huffman 2010-03-03 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
2010-03-03 wenzelm 2010-03-03 merged, resolving some basic conflicts;
2010-03-02 huffman 2010-03-02 fixrec and repdef modules import holcf_library
2010-03-02 huffman 2010-03-02 proper names for types cfun, sprod, ssum
2010-03-02 huffman 2010-03-02 move take-related definitions and proofs to new module; simplify map_of_typ functions
2010-03-01 huffman 2010-03-01 generate take_take rules
2010-03-01 huffman 2010-03-01 add function define_take_functions
2010-02-28 huffman 2010-02-28 domain_isomorphism package proves deflation rules for map functions
2010-02-28 huffman 2010-02-28 store deflation thms for map functions in theory data
2010-02-28 huffman 2010-02-28 move common functions into new file holcf_library.ML
2010-02-28 huffman 2010-02-28 move some powerdomain stuff into a new file
2010-03-03 wenzelm 2010-03-03 cleanup type translations;
2009-11-19 huffman 2009-11-19 store map_ID thms in theory data; automate proofs of reach lemmas
2009-11-19 huffman 2009-11-19 set up domain_isomorphism package in Representable.thy
2009-11-19 huffman 2009-11-19 add lemma isodefl_cprod
2009-11-19 huffman 2009-11-19 change naming convention for deflation combinators
2009-11-18 huffman 2009-11-18 remove one_typ and tr_typ; add abs/rep lemmas
2009-11-13 huffman 2009-11-13 automate definition of representable domains from algebraic deflations
2009-11-10 huffman 2009-11-10 add title/author block
2009-11-10 huffman 2009-11-10 theory of representable cpos