src/HOL/Tools/recdef.ML
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-03-22 wenzelm 2014-03-22 avoid hard-wired theory names;
2014-03-18 wenzelm 2014-03-18 tuned signature;
2014-03-10 wenzelm 2014-03-10 clarified Args.check_src: retain name space information for error output; tuned signature;
2014-03-10 wenzelm 2014-03-10 clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-11-26 wenzelm 2012-11-26 tuned command descriptions;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-03-21 wenzelm 2012-03-21 optional 'includes' element for long theorem statements; tuned signatures;
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-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-01-11 wenzelm 2012-01-11 refer to imp_cong from HOL, not Drule (!) -- cf. 4ed94d92ae19;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-12 wenzelm 2011-05-12 prefer Proof.context over old-style claset/simpset; canonical argument order;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-16 wenzelm 2010-05-16 prefer structure Parse_Spec;
2010-05-12 wenzelm 2010-05-12 updated/unified some legacy warnings;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
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"