src/HOLCF/Universal.thy
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-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-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-22 huffman 2010-03-22 remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2010-03-14 huffman 2010-03-14 use headers consistently
2010-03-10 huffman 2010-03-10 adapt HOLCF to use Nat_Bijection library
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-10-22 wenzelm 2009-10-22 renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);
2009-10-18 wenzelm 2009-10-18 fixed proof (cf. d1d4d7a08a66);
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;
2009-03-16 huffman 2009-03-16 clean up proofs
2009-03-13 huffman 2009-03-13 introduce new helper functions; clean up proofs
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-11-25 huffman 2008-11-25 renamed lemma compact_minimal to compact_bot_minimal
2008-07-01 huffman 2008-07-01 universal bifinite domain