src/HOL/UNITY/UNITY_tactics.ML
2015-07-24 wenzelm 2015-07-24 proper context;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-19 wenzelm 2015-03-19 more position information;
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-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2011-10-13 haftmann 2011-10-13 tuned
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-05-12 wenzelm 2011-05-12 prefer Proof.context over old-style clasimpset;
2010-07-22 wenzelm 2010-07-22 updated some headers;
2010-01-03 paulson 2010-01-03 removed legacy asm_lr_simp_tac
2009-03-20 wenzelm 2009-03-20 eliminated old Addsimps;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-14 wenzelm 2008-06-14 proper context for tactics derived from res_inst_tac;
2007-08-03 wenzelm 2007-08-03 misc cleanup of ML bindings (for multihreading);
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings;
2003-02-08 paulson 2003-02-08 converting HOL/UNITY to use unconditional fairness
2003-01-31 paulson 2003-01-31 conversion to new-style theories and tidying
2003-01-30 paulson 2003-01-30 conversion of UNITY theories to new-style
2003-01-30 paulson 2003-01-30 converting more UNITY theories to new-style
2003-01-29 paulson 2003-01-29 converted more UNITY theories to new-style
2003-01-29 paulson 2003-01-29 converting UNITY to new-style theories
2003-01-24 paulson 2003-01-24 More conversion of UNITY to Isar new-style theories