| Sun, 26 Jul 2015 17:24:54 +0200 | wenzelm | updated to infer_instantiate; | file | diff | annotate |
| Fri, 06 Mar 2015 23:56:43 +0100 | wenzelm | clarified context; | file | diff | annotate |
| Fri, 06 Mar 2015 15:58:56 +0100 | wenzelm | Thm.cterm_of and Thm.ctyp_of operate on local context; | file | diff | annotate |
| Sun, 09 Nov 2014 14:08:00 +0100 | wenzelm | proper context for compose_tac, Splitter.split_tac (relevant for unify trace options); | file | diff | annotate |
| Thu, 20 Feb 2014 19:32:20 +0100 | wenzelm | tuned whitespace; | file | diff | annotate |
| Sat, 14 Jan 2012 21:16:15 +0100 | wenzelm | discontinued old-style Term.list_abs in favour of plain Term.abs; | file | diff | annotate |
| Mon, 28 Sep 2009 22:47:34 +0200 | wenzelm | moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception); | file | diff | annotate |