2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
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-20 wenzelm 2014-12-20 proper context for "net" tactics; avoid implicit Tactic.build_net -- make its operational behavior explicit in application;
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;
2011-01-07 wenzelm 2011-01-07 do not open ML structures;
2010-08-17 haftmann 2010-08-17 more antiquotations
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2007-09-15 haftmann 2007-09-15 fixed title
1999-07-27 paulson 1999-07-27 split off modal.ML from provers.ML