equal
deleted
inserted
replaced
84 ? filter_out (curry (op =) Induction o snd o snd o fst |
84 ? filter_out (curry (op =) Induction o snd o snd o fst |
85 o untranslated_fact) |
85 o untranslated_fact) |
86 |> take num_facts} |
86 |> take num_facts} |
87 fun really_go () = |
87 fun really_go () = |
88 problem |
88 problem |
89 |> get_minimizing_prover ctxt mode name params minimize_command |
89 |> get_minimizing_prover ctxt mode |
|
90 (mash_learn_proof ctxt params (prop_of goal) |
|
91 (map untranslated_fact facts)) |
|
92 name params minimize_command |
90 |> (fn {outcome, preplay, message, message_tail, ...} => |
93 |> (fn {outcome, preplay, message, message_tail, ...} => |
91 (if outcome = SOME ATP_Proof.TimedOut then timeoutN |
94 (if outcome = SOME ATP_Proof.TimedOut then timeoutN |
92 else if is_some outcome then noneN |
95 else if is_some outcome then noneN |
93 else someN, fn () => message (preplay ()) ^ message_tail)) |
96 else someN, fn () => message (preplay ()) ^ message_tail)) |
94 fun go () = |
97 fun go () = |