equal
deleted
inserted
replaced
228 future_result ctxt' |
228 future_result ctxt' |
229 (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri} |
229 (Execution.fork {name = "Goal.prove", pos = Position.thread_data (), pri = the fork_pri} |
230 result) |
230 result) |
231 (Thm.term_of stmt); |
231 (Thm.term_of stmt); |
232 in |
232 in |
233 Conjunction.elim_balanced (length props) res |
233 res |
|
234 |> length props > 1 ? Thm.norm_proof |
|
235 |> Conjunction.elim_balanced (length props) |
234 |> map (Assumption.export false ctxt' ctxt) |
236 |> map (Assumption.export false ctxt' ctxt) |
235 |> Variable.export ctxt' ctxt |
237 |> Variable.export ctxt' ctxt |
236 |> map Drule.zero_var_indexes |
238 |> map Drule.zero_var_indexes |
237 end; |
239 end; |
238 |
240 |