equal
deleted
inserted
replaced
21 val do_it = false (* switch to "true" to generate the files *) |
21 val do_it = false (* switch to "true" to generate the files *) |
22 val thy = @{theory List} |
22 val thy = @{theory List} |
23 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
23 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
24 val prover = hd provers |
24 val prover = hd provers |
25 *} |
25 *} |
|
26 |
26 ML {* |
27 ML {* |
27 if do_it then |
28 if do_it then |
28 generate_accessibility thy false "/tmp/mash_accessibility" |
29 generate_accessibility @{context} thy false "/tmp/mash_accessibility" |
29 else |
30 else |
30 () |
31 () |
31 *} |
32 *} |
32 |
33 |
33 ML {* |
34 ML {* |
37 () |
38 () |
38 *} |
39 *} |
39 |
40 |
40 ML {* |
41 ML {* |
41 if do_it then |
42 if do_it then |
42 generate_isar_dependencies thy false "/tmp/mash_dependencies" |
43 generate_isar_dependencies @{context} thy false "/tmp/mash_dependencies" |
43 else |
44 else |
44 () |
45 () |
45 *} |
46 *} |
46 |
47 |
47 ML {* |
48 ML {* |