equal
deleted
inserted
replaced
1 theory ATP_Export |
|
2 imports Complex_Main |
|
3 uses "atp_export.ML" |
|
4 begin |
|
5 |
|
6 ML {* |
|
7 open ATP_Problem; |
|
8 open ATP_Export; |
|
9 *} |
|
10 |
|
11 ML {* |
|
12 val do_it = false; (* switch to "true" to generate the files *) |
|
13 val thy = @{theory Complex_Main}; |
|
14 val ctxt = @{context} |
|
15 *} |
|
16 |
|
17 ML {* |
|
18 if do_it then |
|
19 "/tmp/axs_mono_simple.dfg" |
|
20 |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted) |
|
21 "mono_simple" |
|
22 else |
|
23 () |
|
24 *} |
|
25 |
|
26 ML {* |
|
27 if do_it then |
|
28 "/tmp/infs_poly_guards.tptp" |
|
29 |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards" |
|
30 else |
|
31 () |
|
32 *} |
|
33 |
|
34 ML {* |
|
35 if do_it then |
|
36 "/tmp/infs_poly_tags.tptp" |
|
37 |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags" |
|
38 else |
|
39 () |
|
40 *} |
|
41 |
|
42 ML {* |
|
43 if do_it then |
|
44 "/tmp/infs_poly_tags_uniform.tptp" |
|
45 |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform" |
|
46 else |
|
47 () |
|
48 *} |
|
49 |
|
50 ML {* |
|
51 if do_it then |
|
52 "/tmp/graph.out" |> generate_tptp_graph_file_for_theory ctxt thy |
|
53 else |
|
54 () |
|
55 *} |
|
56 |
|
57 end |
|