src/HOL/Tools/Function/function_lib.ML
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-11-12 blanchet 2013-11-12 ported part of function package to new 'Ctr_Sugar' abstraction
2013-11-12 blanchet 2013-11-12 undid copy-paste
2011-10-16 wenzelm 2011-10-16 added Term.dummy_pattern conveniences;
2011-04-27 wenzelm 2011-04-27 merged
2011-04-27 krauss 2011-04-27 inlined Function_Lib.replace_frees, which is used only once
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-27 wenzelm 2011-04-27 eliminated obsolete Function_Lib.frees_in_term; simplified;
2010-12-13 krauss 2010-12-13 eliminated dest_all_all_ctx
2010-12-13 krauss 2010-12-13 private term variant of Variable.focus
2010-12-12 krauss 2010-12-12 added signature; more honest header
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-10-22 krauss 2010-10-22 some cleanup in Function_Lib
2010-09-28 krauss 2010-09-28 consolidated tupled_lambda; moved to structure HOLogic
2010-07-08 haftmann 2010-07-08 tuned titles
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2009-11-23 krauss 2009-11-23 eliminated dead code and some unused bindings, reported by polyml
2009-11-11 haftmann 2009-11-11 tuned
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files