| Wed, 22 Aug 2012 22:55:41 +0200 | wenzelm | prefer ML_file over old uses; | file | diff | annotate |
| Fri, 16 Mar 2012 14:46:13 +0100 | wenzelm | refute_params are given in *this* theory; | file | diff | annotate |
| Thu, 15 Mar 2012 22:08:53 +0100 | wenzelm | declare command keywords via theory header, including strict checking outside Pure; | file | diff | annotate |
| Tue, 26 Oct 2010 12:17:19 +0200 | blanchet | reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers | file | diff | annotate |
| Mon, 25 Oct 2010 13:34:57 +0200 | haftmann | moved sledgehammer to Plain; tuned dependencies | file | diff | annotate |
| Mon, 04 Oct 2010 22:45:09 +0200 | blanchet | move Metis into Plain | file | diff | annotate |
| Thu, 02 Sep 2010 17:12:16 +0200 | wenzelm | just one refute.ML; | file | diff | annotate |