96 max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, |
96 max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, |
97 compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize, |
97 compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize, |
98 slice = Time.zeroTime, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} |
98 slice = Time.zeroTime, timeout = timeout, preplay_timeout = preplay_timeout, 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)], found_proof = I} |
101 facts = ("", 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 |