96 isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, |
96 isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, |
97 slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
97 slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
98 expect = ""} |
98 expect = ""} |
99 val problem = |
99 val problem = |
100 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
100 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
101 factss = [("", facts)]} |
101 factss = [("", facts)], found_proof = I} |
102 val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, |
102 val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, |
103 message} = |
103 message} = |
104 prover params problem |
104 prover params problem |
105 val result as {outcome, ...} = |
105 val result as {outcome, ...} = |
106 if is_none outcome0 andalso |
106 if is_none outcome0 andalso |