2014-11-02 wenzelm 2014-11-02 modernized header;
2014-08-16 wenzelm 2014-08-16 clarified order of rules for match_tac/resolve_tac;
2014-08-16 wenzelm 2014-08-16 prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-10-09 huffman 2012-10-09 removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands; removed '(open)', '(set_name)' and '(open set_name)' options
2011-11-30 wenzelm 2011-11-30 prefer cpodef without extra definition;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-06 wenzelm 2011-04-06 separate structure Term_Position; dismantled remains of structure Type_Ext;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-03-29 wenzelm 2011-03-29 tuned headers;
2011-03-22 wenzelm 2011-03-22 more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-03-22 wenzelm 2011-03-22 enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;
2011-01-08 huffman 2011-01-08 use proper syntactic types for 'syntax' commands
2011-01-08 huffman 2011-01-08 make print translation for Abs_cfun consistent with other binders: prevent eta-contraction, but don't force eta-expansion
2011-01-04 huffman 2011-01-04 change some lemma names containing 'UU' to 'bottom'
2010-12-23 huffman 2010-12-23 replaced separate lemmas seq{1,2,3} with seq_simps
2010-12-20 huffman 2010-12-20 beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction
2010-12-06 huffman 2010-12-06 remove lemma cont_cfun; rename thelub_cfun to lub_cfun
2010-12-06 huffman 2010-12-06 rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
2010-12-06 huffman 2010-12-06 add lemmas lub_APP, lub_LAM
2010-11-30 huffman 2010-11-30 change cpodef-generated cont_Rep rules to cont2cont format
2010-11-27 huffman 2010-11-27 add lemma cont2cont_if_bottom
2010-11-27 huffman 2010-11-27 moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;