| Mon, 13 Apr 2015 13:03:41 +0200 | traytel | call Goal.prove only once for a quadratic number of theorems | file | diff | annotate |
| Sat, 07 Mar 2015 00:45:15 +0100 | wenzelm | tuned; | 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 |
| Wed, 04 Mar 2015 19:53:18 +0100 | wenzelm | tuned signature -- prefer qualified names; | 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 |
| Wed, 01 Jan 2014 14:29:22 +0100 | wenzelm | clarified simplifier context; | file | diff | annotate |
| Sat, 14 Dec 2013 17:28:05 +0100 | wenzelm | proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; | file | diff | annotate |
| Mon, 09 Dec 2013 09:44:57 +0100 | blanchet | tuning -- moved ML files to subdirectory | file | diff | annotate | base |