equal
deleted
inserted
replaced
88 let |
88 let |
89 val facts = |
89 val facts = |
90 facts |
90 facts |
91 |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t |
91 |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t |
92 |> take (the max_facts) |
92 |> take (the max_facts) |
93 val res as {outcome, ...} = run_prover ctxt params prover facts goal |
93 val res as {outcome, ...} = |
|
94 run_prover_for_mash ctxt params prover facts goal |
94 val _ = if is_none outcome then ok := !ok + 1 else () |
95 val _ = if is_none outcome then ok := !ok + 1 else () |
95 in str_of_res heading facts res end |
96 in str_of_res heading facts res end |
96 val iter_s = prove iter_ok iterN iter_facts |
97 val iter_s = prove iter_ok iterN iter_facts |
97 val mash_s = prove mash_ok mashN mash_facts |
98 val mash_s = prove mash_ok mashN mash_facts |
98 val mesh_s = prove mesh_ok meshN mesh_facts |
99 val mesh_s = prove mesh_ok meshN mesh_facts |