src/Tools/cong_tac.ML
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate;
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;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-02-20 wenzelm 2014-02-20 tuned whitespace;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2009-09-28 wenzelm 2009-09-28 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);