equal
deleted
inserted
replaced
116 val proof_method_names = [metisN, smtN] |
116 val proof_method_names = [metisN, smtN] |
117 val is_proof_method = member (op =) proof_method_names |
117 val is_proof_method = member (op =) proof_method_names |
118 |
118 |
119 val is_atp = member (op =) o supported_atps |
119 val is_atp = member (op =) o supported_atps |
120 |
120 |
121 fun remotify_atp_if_supported_and_not_already_remote thy name = |
121 fun remotify_atp_if_not_installed thy name = |
122 if String.isPrefix remote_prefix name then |
122 if is_atp thy name then |
|
123 if String.isPrefix remote_prefix name orelse is_atp_installed thy name then |
|
124 SOME name |
|
125 else |
|
126 let val remote_name = remote_prefix ^ name in |
|
127 if is_atp thy remote_name then SOME remote_name else NONE |
|
128 end |
|
129 else |
123 SOME name |
130 SOME name |
124 else |
|
125 let val remote_name = remote_prefix ^ name in |
|
126 if is_atp thy remote_name then SOME remote_name else NONE |
|
127 end |
|
128 |
|
129 fun remotify_atp_if_not_installed thy name = |
|
130 if is_atp thy name andalso is_atp_installed thy name then SOME name |
|
131 else remotify_atp_if_supported_and_not_already_remote thy name |
|
132 |
131 |
133 type params = |
132 type params = |
134 {debug : bool, |
133 {debug : bool, |
135 verbose : bool, |
134 verbose : bool, |
136 overlord : bool, |
135 overlord : bool, |