src/HOLCF/Algebraic.thy
2010-11-10 huffman 2010-11-10 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-10-29 huffman 2010-10-29 renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
2010-10-19 huffman 2010-10-19 replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
2010-10-11 huffman 2010-10-11 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
2010-10-07 huffman 2010-10-07 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
2010-10-07 huffman 2010-10-07 add lemma typedef_ideal_completion
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 lemmas finite_deflation_imp_compact, cast_below_cast_iff
2010-10-05 Brian Huffman 2010-10-05 move lemmas to Deflation.thy
2010-10-02 huffman 2010-10-02 minimize theory imports
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 renamed expand_*_eq in HOLCF as well
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-11-09 huffman 2009-11-09 add in_deflation relation, more lemmas about cast
2009-05-15 huffman 2009-05-15 continuity proofs for approx function on deflations; lemma cast_below_imp_below
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;
2008-12-30 ballarin 2008-12-30 Merged.
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-10-16 ballarin 2008-10-16 More occurrences of 'includes' gone.
2008-07-01 huffman 2008-07-01 range_composition no longer in simp set
2008-07-01 huffman 2008-07-01 theory of algebraic deflations