src/HOL/Tools/Function/function_common.ML
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-11-10 haftmann 2013-11-10 qualifed popular user space names
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
2012-10-28 Christian Urban 2012-10-28 added function store_termination_rule to the signature, as it is used in Nominal2
2012-10-21 wenzelm 2012-10-21 removed dead code;
2012-10-21 wenzelm 2012-10-21 proper signatures;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-02-15 wenzelm 2012-02-15 discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
2011-12-29 wenzelm 2011-12-29 comments;
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-10-28 wenzelm 2011-10-28 tuned signature -- refined terminology;
2011-08-21 wenzelm 2011-08-21 tuned Parse.group: delayed failure message;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-24 wenzelm 2011-03-24 indentation;
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-12 krauss 2010-12-12 tuned headers
2010-09-10 krauss 2010-09-10 improved error message for common mistake (fun f where "g x = ...")
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-08-26 wenzelm 2010-08-26 more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
2010-08-26 wenzelm 2010-08-26 theory data merge: prefer left side uniformly;
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-05 haftmann 2010-05-05 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-04-28 krauss 2010-04-28 default termination prover as plain tactic
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-19 krauss 2009-11-19 check if equations are present for all functions to avoid low-level exception later
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-02 krauss 2009-11-02 conceal partial rules depending on config flag (i.e. when called via "fun")
2009-11-01 wenzelm 2009-11-01 adapted Item_Net; tuned;
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