src/HOL/Multivariate_Analysis/normarith.ML
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
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 clarified signature;
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-10-08 wenzelm 2014-10-08 eliminated some exotic combinators;
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-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-06-22 huffman 2012-06-22 avoid duplicate simp rules in norm_arith tactic
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-08-22 huffman 2011-08-22 avoid warnings
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
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;
2010-11-26 wenzelm 2010-11-26 just one version of fold_rev2;
2010-11-26 wenzelm 2010-11-26 eliminated some clones of eq_list;
2010-09-02 haftmann 2010-09-02 Table.map replaces Table.map'
2010-07-08 haftmann 2010-07-08 tuned titles
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-15 wenzelm 2010-05-15 removed unused conversions;
2010-05-15 wenzelm 2010-05-15 tuned header; tuned white space;
2010-05-15 wenzelm 2010-05-15 moved normarith.ML where it is actually used; less inaccurate dependencies;