| author | blanchet |
| Tue, 10 Jul 2012 23:36:03 +0200 | |
| changeset 48235 | 40655464a93b |
| parent 48234 | 06216c789ac9 |
| child 48236 | e174ecc4f5a4 |
| permissions | -rw-r--r-- |
| 48234 | 1 |
(* Title: HOL/TPTP/MaSh_Import.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* MaSh Importer *}
|
|
6 |
||
7 |
theory MaSh_Import |
|
8 |
imports MaSh_Export |
|
9 |
uses "mash_import.ML" |
|
10 |
begin |
|
11 |
||
| 48235 | 12 |
ML {*
|
13 |
open MaSh_Import |
|
14 |
*} |
|
15 |
||
16 |
ML {*
|
|
17 |
val do_it = true (* switch to "true" to generate the files *); |
|
18 |
val thy = @{theory List}
|
|
19 |
*} |
|
20 |
||
21 |
ML {*
|
|
22 |
if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions2"
|
|
23 |
else () |
|
24 |
*} |
|
25 |
||
| 48234 | 26 |
end |