src/HOL/Tools/Function/function.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-02-12 blanchet 2014-02-12 transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-09-12 krauss 2013-09-12 omit automatic Induct.cases_pred declaration, which breaks many existing proofs
2013-09-08 krauss 2013-09-08 clarified
2013-09-08 Manuel Eberl 2013-09-08 generate elim rules for elimination of function equalities; added fun_cases command; recover proper cases rules for mutual recursive case (no sum types)
2013-06-16 krauss 2013-06-16 export dom predicate in the info record
2013-06-16 krauss 2013-06-16 export cases rule in the info record
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-01-08 wenzelm 2013-01-08 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
2012-10-21 wenzelm 2012-10-21 recovered explicit error message, which was lost in b8570ea1ce25;
2012-08-29 wenzelm 2012-08-29 more precise indentation;
2012-04-23 wenzelm 2012-04-23 more standard method setup;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-11-19 wenzelm 2011-11-19 added ML antiquotation @{attributes};
2011-10-28 wenzelm 2011-10-28 uniform Local_Theory.declaration with explicit params;
2011-10-28 wenzelm 2011-10-28 tuned signature -- refined terminology;
2011-08-17 wenzelm 2011-08-17 less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
2011-08-13 wenzelm 2011-08-13 less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;
2011-08-08 wenzelm 2011-08-08 slightly more uniform messages;
2011-06-08 wenzelm 2011-06-08 pervasive Output operations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-02-25 krauss 2011-02-25 removed support for tail-recursion from function package (now implemented by partial_function)
2010-12-29 krauss 2010-12-29 function (default) is legacy feature
2010-12-27 krauss 2010-12-27 function (tailrec) is a legacy feature
2010-12-12 krauss 2010-12-12 tuned headers
2010-10-22 krauss 2010-10-22 some cleanup in Function_Lib
2010-09-28 krauss 2010-09-28 no longer declare .psimps rules as [simp]. This regularly caused confusion (e.g., they show up in simp traces when the regular simp rules are disabled). In the few places where the rules are used, explicitly mentioning them actually clarifies the proof text.
2010-07-08 haftmann 2010-07-08 tuned titles
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