equal
deleted
inserted
replaced
1 theory TPTP_Export |
|
2 imports Complex_Main |
|
3 uses "tptp_export.ML" |
|
4 begin |
|
5 |
|
6 ML {* |
|
7 val do_it = false; (* switch to true to generate files *) |
|
8 val thy = @{theory Complex_Main}; |
|
9 val ctxt = @{context} |
|
10 *} |
|
11 |
|
12 ML {* |
|
13 if do_it then |
|
14 TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true |
|
15 "/tmp/infs_full_types.tptp" |
|
16 else |
|
17 () |
|
18 *} |
|
19 |
|
20 ML {* |
|
21 if do_it then |
|
22 TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy false |
|
23 "/tmp/infs_partial_types.tptp" |
|
24 else |
|
25 () |
|
26 *} |
|
27 |
|
28 ML {* |
|
29 if do_it then |
|
30 TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy |
|
31 "/tmp/graph.out" |
|
32 else |
|
33 () |
|
34 *} |
|
35 |
|
36 end |
|