2011-04-03 wenzelm 2011-04-03 added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;
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-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-01 huffman 2010-12-01 domain package generates non-authentic syntax rules for parsing only
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;