author | blanchet |
Wed, 11 Jul 2012 21:43:19 +0200 | |
changeset 48251 | 6cdcfbddc077 |
parent 48250 | 1065c307fafe |
child 48284 | a3cb8901d60c |
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 |
||
48236 | 12 |
declare [[sledgehammer_instantiate_inducts]] |
13 |
||
48235 | 14 |
ML {* |
15 |
open MaSh_Import |
|
16 |
*} |
|
17 |
||
18 |
ML {* |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
19 |
val do_it = false (* switch to "true" to generate the files *); |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
20 |
val thy = @{theory List}; |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
21 |
val params = Sledgehammer_Isar.default_params @{context} [] |
48235 | 22 |
*} |
23 |
||
24 |
ML {* |
|
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
25 |
if do_it then |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
26 |
import_and_evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list" |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
27 |
else |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
28 |
() |
48235 | 29 |
*} |
30 |
||
48234 | 31 |
end |