| Sat, 02 Apr 2016 23:29:05 +0200 | wenzelm | prefer infix operations; | file | diff | annotate |
| Mon, 01 Feb 2016 19:57:58 +0100 | blanchet | preplaying of 'smt' and 'metis' more in sync with actual method | file | diff | annotate |
| Fri, 02 Oct 2015 21:15:25 +0200 | blanchet | further reduced dependency on legacy async thread manager | file | diff | annotate |
| Thu, 28 May 2015 09:50:17 +0200 | blanchet | took out Sledgehammer minimizer optimization that breaks things | file | diff | annotate |
| Thu, 28 Aug 2014 16:58:27 +0200 | blanchet | removed show stuttering | file | diff | annotate |
| Thu, 28 Aug 2014 16:58:27 +0200 | blanchet | made trace more informative when minimization is enabled | file | diff | annotate |
| Thu, 28 Aug 2014 16:58:27 +0200 | blanchet | tuned tracing output (indirectly) | file | diff | annotate |
| Mon, 04 Aug 2014 13:13:10 +0200 | blanchet | sort facts in minimizer as well | file | diff | annotate |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | tuning | file | diff | annotate |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | simplified minimization logic | file | diff | annotate |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | tuning | file | diff | annotate |
| Wed, 30 Jul 2014 23:52:56 +0200 | blanchet | tuned ML function name | file | diff | annotate |
| Fri, 25 Jul 2014 12:20:48 +0200 | blanchet | faster minimization by not adding facts that are already in the simpset | file | diff | annotate |
| Thu, 22 May 2014 03:29:36 +0200 | blanchet | tuning | file | diff | annotate |
| Thu, 13 Feb 2014 13:16:17 +0100 | blanchet | avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures | file | diff | annotate |
| Tue, 04 Feb 2014 23:11:18 +0100 | blanchet | tuned slack | file | diff | annotate |
| Tue, 04 Feb 2014 01:03:28 +0100 | blanchet | tuning | file | diff | annotate |
| Mon, 03 Feb 2014 19:32:02 +0100 | blanchet | generate comments in Isar proofs | file | diff | annotate |
| Mon, 03 Feb 2014 19:32:02 +0100 | blanchet | keep all proof methods in data structure until the end, to enhance debugging output | file | diff | annotate |
| Mon, 03 Feb 2014 16:53:58 +0100 | blanchet | renamed ML file | file | diff | annotate |
| Mon, 03 Feb 2014 11:58:38 +0100 | blanchet | tuned data structure | file | diff | annotate |
| Mon, 03 Feb 2014 11:30:53 +0100 | blanchet | more flexible compression, choosing whichever proof method works | file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | tuning | file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | centralize more preplaying | file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | tuning | file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | centralize preplaying | file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | tuned | file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | more data structure rationalization | file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | tuning | file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | more data structure rationalization | file | diff | annotate |