src/HOL/Decision_Procs/approximation.ML
2016-12-06 wenzelm 2016-12-06 avoid spurious messages;
2016-09-21 immler 2016-09-21 provide more information on error
2016-09-21 immler 2016-09-21 approximation: rewrite for reduction to base expressions
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-02-23 nipkow 2016-02-23 more canonical names
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-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-30 eberlm 2015-03-30 exposed approximation in 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-12-22 wenzelm 2014-12-22 tuned;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-05-09 haftmann 2014-05-09 prefer separate command for approximation
2014-05-01 haftmann 2014-05-01 separate ML module