equal
deleted
inserted
replaced
|
1 theory ATP_Export |
|
2 imports Complex_Main |
|
3 uses "atp_export.ML" |
|
4 begin |
|
5 |
|
6 ML {* |
|
7 val do_it = false; (* switch to "true" to generate the files *) |
|
8 val thy = @{theory Complex_Main}; |
|
9 val ctxt = @{context} |
|
10 *} |
|
11 |
|
12 ML {* |
|
13 if do_it then |
|
14 ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds" |
|
15 "/tmp/infs_poly_preds.tptp" |
|
16 else |
|
17 () |
|
18 *} |
|
19 |
|
20 ML {* |
|
21 if do_it then |
|
22 ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags" |
|
23 "/tmp/infs_poly_tags.tptp" |
|
24 else |
|
25 () |
|
26 *} |
|
27 |
|
28 ML {* |
|
29 if do_it then |
|
30 ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy" |
|
31 "/tmp/infs_poly_tags_heavy.tptp" |
|
32 else |
|
33 () |
|
34 *} |
|
35 |
|
36 ML {* |
|
37 if do_it then |
|
38 ATP_Export.generate_tptp_graph_file_for_theory ctxt thy |
|
39 "/tmp/graph.out" |
|
40 else |
|
41 () |
|
42 *} |
|
43 |
|
44 end |