src/HOL/HOLCF/Tools/cpodef.ML
2012-10-12 wenzelm 2012-10-12 discontinued typedef with alternative name;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with implicit set_def;
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
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-13 wenzelm 2012-03-13 more explicit indication of def names;
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-08-08 huffman 2011-08-08 HOLCF: fix warnings about unreferenced identifiers
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-29 wenzelm 2011-03-29 tuned headers;
2011-01-04 huffman 2011-01-04 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax; removed redundant lemma UU_least
2010-12-19 huffman 2010-12-19 switch to transparent ascription, to avoid warning messages
2010-12-06 huffman 2010-12-06 pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
2010-12-06 huffman 2010-12-06 cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo
2010-12-01 huffman 2010-12-01 tuned cpodef code
2010-11-30 huffman 2010-11-30 remove gratuitous semicolons from ML code
2010-11-27 huffman 2010-11-27 moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;