equal
deleted
inserted
replaced
17 |
17 |
18 fun run_atp force_full_types timeout i n ctxt goal name = |
18 fun run_atp force_full_types timeout i n ctxt goal name = |
19 let |
19 let |
20 val chained_ths = [] (* a tactic has no chained ths *) |
20 val chained_ths = [] (* a tactic has no chained ths *) |
21 val params as {relevance_thresholds, max_relevant, slicing, ...} = |
21 val params as {relevance_thresholds, max_relevant, slicing, ...} = |
22 ((if force_full_types then [("full_types", "true")] else []) |
22 ((if force_full_types then [("sound", "true")] else []) |
23 @ [("timeout", string_of_int (Time.toSeconds timeout))]) |
23 @ [("timeout", string_of_int (Time.toSeconds timeout))]) |
24 (* @ [("overlord", "true")] *) |
24 (* @ [("overlord", "true")] *) |
25 |> Sledgehammer_Isar.default_params ctxt |
25 |> Sledgehammer_Isar.default_params ctxt |
26 val prover = |
26 val prover = |
27 Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name |
27 Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name |