src/HOL/HOLCF/Cfun.thy
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;