equal
deleted
inserted
replaced
50 () |
50 () |
51 *} |
51 *} |
52 |
52 |
53 ML {* |
53 ML {* |
54 if do_it then |
54 if do_it then |
55 generate_isar_dependencies @{context} thys false (prefix ^ "mash_dependencies") |
55 generate_isar_dependencies @{context} thys false |
|
56 (prefix ^ "mash_dependencies") |
56 else |
57 else |
57 () |
58 () |
58 *} |
59 *} |
59 |
60 |
60 ML {* |
61 ML {* |
64 () |
65 () |
65 *} |
66 *} |
66 |
67 |
67 ML {* |
68 ML {* |
68 if do_it then |
69 if do_it then |
69 generate_mepo_suggestions @{context} params thys 1024 (prefix ^ "mash_mepo_suggestions") |
70 generate_mepo_suggestions @{context} params thys 1024 |
|
71 (prefix ^ "mash_mepo_suggestions") |
70 else |
72 else |
71 () |
73 () |
72 *} |
74 *} |
73 |
75 |
74 ML {* |
76 ML {* |
75 if do_it then |
77 if do_it then |
76 generate_atp_dependencies @{context} params thys false (prefix ^ "mash_atp_dependencies") |
78 generate_prover_dependencies @{context} params thys false |
|
79 (prefix ^ "mash_prover_dependencies") |
77 else |
80 else |
78 () |
81 () |
79 *} |
82 *} |
80 |
83 |
81 ML {* |
84 ML {* |
82 if do_it then |
85 if do_it then |
83 generate_atp_commands @{context} params thys (prefix ^ "mash_atp_commands") |
86 generate_prover_commands @{context} params thys |
|
87 (prefix ^ "mash_prover_commands") |
84 else |
88 else |
85 () |
89 () |
86 *} |
90 *} |
87 |
91 |
88 end |
92 end |