src/HOL/Tools/recdef.ML
2010-03-12 bulwahn 2010-03-12 refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
2010-03-10 haftmann 2010-03-10 recdef is legacy
2010-01-21 bulwahn 2010-01-21 corrected and simplified Spec_Rules registration in the Recdef package
2010-01-20 bulwahn 2010-01-20 added registration of equational theorems from prim_rec and rec_def to Spec_Rules
2009-11-15 wenzelm 2009-11-15 permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-10 wenzelm 2009-11-10 removed unused Quickcheck_RecFun_Simps;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-21 blanchet 2009-10-21 renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-10-02 wenzelm 2009-10-02 eliminated dead code; tuned;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"