src/HOL/Tools/Function/fun.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2013-11-12 blanchet 2013-11-12 ported part of function package to new 'Ctr_Sugar' abstraction
2012-10-21 wenzelm 2012-10-21 proper signatures;
2012-06-06 krauss 2012-06-06 fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-11-25 krauss 2011-11-25 removed obsolete uses of Local_Theory.restore -- package composition P1 #> P2 no longer requires them due to 57def0b39696: P2 finds the results of P1 in the auxiliary context
2011-08-17 wenzelm 2011-08-17 less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
2011-08-17 wenzelm 2011-08-17 export Function_Fun.fun_config for user convenience;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 prefer new-style Name.invents;
2011-06-08 wenzelm 2011-06-08 pervasive Output operations;
2011-05-22 krauss 2011-05-22 fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
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-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-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 clarified signature; simpler implementation in terms of function's tactic interface
2010-04-28 krauss 2010-04-28 default termination prover as plain tactic
2010-04-28 krauss 2010-04-28 ML interface uses plain command names, following conventions from typedef
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-23 krauss 2009-11-23 eliminated dead code and some unused bindings, reported by polyml
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-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
2009-10-23 krauss 2009-10-23 renamed FundefDatatype -> Function_Fun