equal
deleted
inserted
replaced
73 let |
73 let |
74 val fact_names = map fst used_facts |
74 val fact_names = map fst used_facts |
75 |
75 |
76 val {context = ctxt, facts = chained, goal} = Proof.goal state |
76 val {context = ctxt, facts = chained, goal} = Proof.goal state |
77 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt |
77 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt |
78 val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t) |
78 val goal_t = Logic.list_implies (map Thm.prop_of chained @ hyp_ts, concl_t) |
79 |
79 |
80 fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
80 fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
81 | try_methss ress [] = |
81 | try_methss ress [] = |
82 (used_facts, |
82 (used_facts, |
83 (case AList.lookup (op =) ress preferred_meth of |
83 (case AList.lookup (op =) ress preferred_meth of |
303 let |
303 let |
304 val factss = get_factss provers |
304 val factss = get_factss provers |
305 val problem = |
305 val problem = |
306 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
306 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
307 factss = factss} |
307 factss = factss} |
308 val learn = mash_learn_proof ctxt params (prop_of goal) all_facts |
308 val learn = mash_learn_proof ctxt params (Thm.prop_of goal) all_facts |
309 val launch = launch_prover params mode output_result only learn |
309 val launch = launch_prover params mode output_result only learn |
310 in |
310 in |
311 if mode = Auto_Try then |
311 if mode = Auto_Try then |
312 (unknownN, []) |
312 (unknownN, []) |
313 |> fold (fn prover => fn accum as (outcome_code, _) => |
313 |> fold (fn prover => fn accum as (outcome_code, _) => |