src/HOL/Tools/Function/function.ML
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
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-04-30 krauss 2010-04-30 return updated info record after termination proof
2010-04-28 krauss 2010-04-28 return info record (relative to auxiliary context!)
2010-04-28 krauss 2010-04-28 function: sane interface for programmatic use
2010-04-28 krauss 2010-04-28 ML interface uses plain command names, following conventions from typedef
2010-04-28 krauss 2010-04-28 function: better separate Isar integration from actual functionality
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-03-12 bulwahn 2010-03-12 refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-23 bulwahn 2010-02-23 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
2010-01-18 krauss 2010-01-18 function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2010-01-02 krauss 2010-01-02 provide simp and induct rules in Function.info
2010-01-02 krauss 2010-01-02 more official data record Function.info
2009-11-17 wenzelm 2009-11-17 eliminated slightly odd name space grouping -- now managed by Isar toplevel;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-13 wenzelm 2009-11-13 eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-11-10 wenzelm 2009-11-10 removed unused Quickcheck_RecFun_Simps;
2009-11-05 wenzelm 2009-11-05 adapted LocalTheory.declaration;
2009-11-02 krauss 2009-11-02 conceal partial rules depending on config flag (i.e. when called via "fun")
2009-11-02 krauss 2009-11-02 conceal "termination" rule, used only by special tools
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-25 wenzelm 2009-10-25 name space groups are identified by serial, not serial_string;
2009-10-24 krauss 2009-10-24 configuration flag "partials"
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files