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 |
|
|
12 |
ML {*
|
|
13 |
open MaSh_Export
|
|
14 |
*}
|
|
15 |
|
|
16 |
ML {*
|
48235
|
17 |
val do_it = false (* switch to "true" to generate the files *)
|
|
18 |
val thy = @{theory List}
|
48234
|
19 |
*}
|
|
20 |
|
|
21 |
ML {*
|
48235
|
22 |
if do_it then generate_mash_commands thy "/tmp/mash_commands"
|
|
23 |
else ()
|
|
24 |
*}
|
|
25 |
|
|
26 |
ML {*
|
|
27 |
if do_it then generate_mash_features thy false "/tmp/mash_features"
|
|
28 |
else ()
|
48234
|
29 |
*}
|
|
30 |
|
|
31 |
ML {*
|
48235
|
32 |
if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility"
|
|
33 |
else ()
|
48234
|
34 |
*}
|
|
35 |
|
|
36 |
ML {*
|
48235
|
37 |
if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies"
|
|
38 |
else ()
|
48234
|
39 |
*}
|
|
40 |
|
|
41 |
ML {*
|
48235
|
42 |
find_index (curry (op =) 22) [0, 0, 9, 1, 2, 3]
|
48234
|
43 |
*}
|
|
44 |
|
|
45 |
end
|