2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-12 ago refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
2010-01-20 ago added registration of equational theorems from prim_rec and rec_def to Spec_Rules
2009-11-30 ago modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-27 ago renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-21 ago explicitly mark some legacy freeze operations;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-29 ago eliminated some old folds;
2009-10-29 ago standardized filter/filter_out;
2009-10-21 ago renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-02 ago eliminated dead code;
2009-09-28 ago avoid compound fields in datatype info record
2009-09-27 ago registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-07-02 ago renamed NamedThmsFun to Named_Thms;
2009-06-23 ago tuned interfaces of datatype module
2009-06-21 ago simplified names of common datatype types
2009-06-19 ago discontinued ancient tradition to suffix certain ML module names with "_package"