author | blanchet |
Tue, 10 Jul 2012 23:36:03 +0200 | |
changeset 48239 | 0016290f904c |
parent 48235 | 40655464a93b |
child 48245 | 854a47677335 |
permissions | -rw-r--r-- |
48234 | 1 |
(* Title: HOL/TPTP/MaSh_Export.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* MaSh Exporter *} |
|
6 |
||
7 |
theory MaSh_Export |
|
8 |
imports ATP_Theory_Export |
|
9 |
uses "mash_export.ML" |
|
10 |
begin |
|
11 |
||
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
12 |
sledgehammer_params [provers = e, max_relevant = 500] |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
13 |
|
48234 | 14 |
ML {* |
15 |
open MaSh_Export |
|
16 |
*} |
|
17 |
||
18 |
ML {* |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
19 |
val do_it = false (* switch to "true" to generate the files *); |
48235 | 20 |
val thy = @{theory List} |
48234 | 21 |
*} |
22 |
||
23 |
ML {* |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
24 |
if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions" |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
25 |
else () |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
26 |
*} |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
27 |
|
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
28 |
ML {* |
48235 | 29 |
if do_it then generate_mash_commands thy "/tmp/mash_commands" |
30 |
else () |
|
31 |
*} |
|
32 |
||
33 |
ML {* |
|
34 |
if do_it then generate_mash_features thy false "/tmp/mash_features" |
|
35 |
else () |
|
48234 | 36 |
*} |
37 |
||
38 |
ML {* |
|
48235 | 39 |
if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility" |
40 |
else () |
|
48234 | 41 |
*} |
42 |
||
43 |
ML {* |
|
48235 | 44 |
if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies" |
45 |
else () |
|
48234 | 46 |
*} |
47 |
||
48 |
end |