| Fri, 06 Mar 2015 15:58:56 +0100 | wenzelm | Thm.cterm_of and Thm.ctyp_of operate on local context; | file | diff | annotate |
| Wed, 04 Mar 2015 19:53:18 +0100 | wenzelm | tuned signature -- prefer qualified names; | file | diff | annotate |
| Tue, 03 Mar 2015 19:08:04 +0100 | traytel | eliminated some clones of Proof_Context.cterm_of | file | diff | annotate |
| Tue, 10 Feb 2015 14:48:26 +0100 | wenzelm | proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; | file | diff | annotate |
| Mon, 22 Dec 2014 15:50:16 +0100 | wenzelm | tuned; | file | diff | annotate |
| Mon, 03 Nov 2014 14:50:27 +0100 | wenzelm | eliminated unused int_only flag (see also c12484a27367); | file | diff | annotate |
| Fri, 09 May 2014 08:13:36 +0200 | haftmann | prefer separate command for approximation | file | diff | annotate |
| Thu, 01 May 2014 10:20:20 +0200 | haftmann | separate ML module | file | diff | annotate |