| Sat, 22 Dec 2007 14:10:22 +0100 |
wenzelm |
use random_word.ML earlier;
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 14:33:40 +0100 |
wenzelm |
moved Pure/General/random_word.ML to Tools/random_word.ML;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 17:40:48 +0100 |
paulson |
Replaced refs by config params; finer critical section in mets method
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:03 +0100 |
haftmann |
swtiched ATP_Linkup and PreList in theory hierarchy
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 15:05:42 +0200 |
paulson |
removed dead code
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 12:32:58 +0200 |
paulson |
combinator translation
|
file |
diff |
annotate
|
| Wed, 03 Oct 2007 00:02:56 +0200 |
wenzelm |
modernized definitions;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2007 17:55:28 +0200 |
paulson |
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
|
file |
diff |
annotate
|
| Sat, 18 Aug 2007 13:32:18 +0200 |
wenzelm |
renamed ResAtpMethods.setup;
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 15:06:58 +0200 |
paulson |
combining the relevance filter with res_atp
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:38:43 +0200 |
haftmann |
changed import order
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:27:56 +0200 |
haftmann |
simplified HOL bootstrap
|
file |
diff |
annotate
|
| Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 23:19:16 +0200 |
wenzelm |
added Metis setup (from Metis.thy);
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 17:55:12 +0100 |
paulson |
improvements to proof reconstruction. Some files loaded in a different order
|
file |
diff |
annotate
|
| Wed, 03 Jan 2007 10:59:06 +0100 |
paulson |
first version of structured proof reconstruction
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:20:11 +0100 |
haftmann |
removed Extraction dependency
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 21:45:15 +0100 |
wenzelm |
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
|
file |
diff |
annotate
|