381 fun remove_assumption_id assumption_id prems = |
381 fun remove_assumption_id assumption_id prems = |
382 filter_out (curry (op =) assumption_id) prems |
382 filter_out (curry (op =) assumption_id) prems |
383 fun inline_assumption assumption assumption_id |
383 fun inline_assumption assumption assumption_id |
384 (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) = |
384 (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) = |
385 mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt |
385 mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt |
386 (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds |
386 (\<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds |
387 fun find_input_steps_and_inline [] = [] |
387 fun find_input_steps_and_inline [] = [] |
388 | find_input_steps_and_inline |
388 | find_input_steps_and_inline |
389 (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) = |
389 (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) = |
390 if rule = veriT_input_rule then |
390 if rule = veriT_input_rule then |
391 find_input_steps_and_inline (map (inline_assumption concl id') steps) |
391 find_input_steps_and_inline (map (inline_assumption concl id') steps) |