src/HOL/Tools/Function/pat_completeness.ML
2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-03-06 wenzelm 2015-03-06 clarified context;
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-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
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
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-07-08 haftmann 2010-07-08 tuned titles
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files
2009-10-23 krauss 2009-10-23 pat_completeness gets its own file