equal
deleted
inserted
replaced
12 ML {* |
12 ML {* |
13 open MaSh_Export |
13 open MaSh_Export |
14 *} |
14 *} |
15 |
15 |
16 ML {* |
16 ML {* |
17 val do_it = false; (* switch to "true" to generate the files *) |
17 val do_it = false (* switch to "true" to generate the files *) |
18 val thy = @{theory List}; |
18 val thy = @{theory List} |
19 val ctxt = @{context} |
|
20 *} |
19 *} |
21 |
20 |
22 ML {* |
21 ML {* |
23 if do_it then |
22 if do_it then generate_mash_commands thy "/tmp/mash_commands" |
24 "/tmp/mash_sample_problem.out" |
23 else () |
25 |> generate_mash_problem_file_for_theory thy |
|
26 else |
|
27 () |
|
28 *} |
24 *} |
29 |
25 |
30 ML {* |
26 ML {* |
31 if do_it then |
27 if do_it then generate_mash_features thy false "/tmp/mash_features" |
32 "/tmp/mash_features.out" |
28 else () |
33 |> generate_mash_feature_file_for_theory thy false |
|
34 else |
|
35 () |
|
36 *} |
29 *} |
37 |
30 |
38 ML {* |
31 ML {* |
39 if do_it then |
32 if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility" |
40 "/tmp/mash_accessibility.out" |
33 else () |
41 |> generate_mash_accessibility_file_for_theory thy false |
|
42 else |
|
43 () |
|
44 *} |
34 *} |
45 |
35 |
46 ML {* |
36 ML {* |
47 if do_it then |
37 if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies" |
48 "/tmp/mash_dependencies.out" |
38 else () |
49 |> generate_mash_dependency_file_for_theory thy false |
39 *} |
50 else |
40 |
51 () |
41 ML {* |
|
42 find_index (curry (op =) 22) [0, 0, 9, 1, 2, 3] |
52 *} |
43 *} |
53 |
44 |
54 end |
45 end |