equal
deleted
inserted
replaced
169 ) |
169 ) |
170 |
170 |
171 (* The first ATP of the list is used by Auto Sledgehammer. *) |
171 (* The first ATP of the list is used by Auto Sledgehammer. *) |
172 fun default_provers_param_value ctxt = |
172 fun default_provers_param_value ctxt = |
173 \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close> |
173 \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close> |
174 filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps @ tactic_provers) |
174 filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps) |
175 |> implode_param |
175 |> implode_param |
176 |
176 |
177 fun set_default_raw_param param thy = |
177 fun set_default_raw_param param thy = |
178 let val ctxt = Proof_Context.init_global thy in |
178 let val ctxt = Proof_Context.init_global thy in |
179 thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) |
179 thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) |