54 explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), |
54 explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), |
55 max_relevant = NONE, isar_proof = isar_proof, |
55 max_relevant = NONE, isar_proof = isar_proof, |
56 isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
56 isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
57 val axioms = |
57 val axioms = |
58 axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n)) |
58 axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n)) |
59 val {context = ctxt, goal, ...} = Proof.goal state |
59 val {goal, ...} = Proof.goal state |
60 val problem = |
60 val problem = |
61 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
61 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
62 axioms = axioms, only = true} |
62 axioms = axioms, only = true} |
63 val result as {outcome, used_axioms, ...} = prover params (K "") problem |
63 val result as {outcome, used_axioms, ...} = prover params (K "") problem |
64 in |
64 in |