92 type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
92 type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
93 uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, |
93 uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, |
94 induction_rules = induction_rules, max_facts = SOME (length facts), |
94 induction_rules = induction_rules, max_facts = SOME (length facts), |
95 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, |
95 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, |
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, slice = false, |
97 compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize, |
98 minimize = minimize, 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 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} = |