src/HOL/Tools/Function/measure_functions.ML
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
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-08-16 wenzelm 2014-08-16 updated to named_theorems; modernized module name and setup;
2014-03-07 blanchet 2014-03-07 tuning
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-08-26 wenzelm 2010-08-26 more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2009-09-18 haftmann 2009-09-18 tuned const_name antiquotations
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories