equal
deleted
inserted
replaced
8 imports Complex_Main |
8 imports Complex_Main |
9 uses "atp_theory_export.ML" |
9 uses "atp_theory_export.ML" |
10 begin |
10 begin |
11 |
11 |
12 ML {* |
12 ML {* |
13 open ATP_Problem; |
13 open ATP_Problem |
14 open ATP_Theory_Export; |
14 open ATP_Theory_Export |
15 *} |
15 *} |
16 |
16 |
17 ML {* |
17 ML {* |
18 val do_it = false; (* switch to "true" to generate the files *) |
18 val do_it = false (* switch to "true" to generate the files *) |
19 val thy = @{theory List}; |
19 val thy = @{theory List} |
20 val ctxt = @{context} |
20 val ctxt = @{context} |
21 *} |
21 *} |
22 |
22 |
23 ML {* |
23 ML {* |
24 if do_it then |
24 if do_it then |