src/HOL/Tools/recdef.ML
2012-04-27 ago clarified signature;
2012-03-21 ago optional 'includes' element for long theorem statements;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 ago prefer formally checked @{keyword} parser;
2012-03-15 ago declare minor keywords via theory header;
2012-01-11 ago refer to imp_cong from HOL, not Drule (!) -- cf. 4ed94d92ae19;
2011-11-23 ago modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-08-02 ago moved recdef package to HOL/Library/Old_Recdef.thy
2011-06-08 ago more robust exception pattern General.Subscript;
2011-05-13 ago clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-12 ago prefer Proof.context over old-style claset/simpset;
2011-04-16 ago modernized structure Proof_Context;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-16 ago prefer structure Parse_Spec;
2010-05-12 ago updated/unified some legacy warnings;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-12 ago refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
2010-03-10 ago recdef is legacy
2010-01-21 ago corrected and simplified Spec_Rules registration in the Recdef package
2010-01-20 ago added registration of equational theorems from prim_rec and rec_def to Spec_Rules
2009-11-15 ago permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
2009-11-12 ago eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-10 ago removed unused Quickcheck_RecFun_Simps;
2009-11-08 ago adapted Theory_Data;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-10-28 ago conceal internal bindings;
2009-10-21 ago renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-15 ago replaced String.concat by implode;
2009-10-02 ago eliminated dead code;
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-02 ago renamed NamedThmsFun to Named_Thms;
2009-06-19 ago discontinued ancient tradition to suffix certain ML module names with "_package"