src/HOL/HOLCF/ex/Pattern_Match.thy
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
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-03-13 wenzelm 2012-03-13 more explicit indication of def names;
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
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-08 huffman 2011-01-08 types -> type_synonym
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-11-30 huffman 2010-11-30 change cpodef-generated cont_Rep rules to cont2cont format
2010-11-27 huffman 2010-11-27 moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;