736 fun mk_prop_of_term concl = |
736 fun mk_prop_of_term concl = |
737 concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close> |
737 concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close> |
738 fun remove_assumption_id assumption_id prems = |
738 fun remove_assumption_id assumption_id prems = |
739 filter_out (curry (op =) assumption_id) prems |
739 filter_out (curry (op =) assumption_id) prems |
740 fun add_assumption assumption concl = |
740 fun add_assumption assumption concl = |
741 \<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl |
741 \<^Const>\<open>Pure.imp for \<open>mk_prop_of_term assumption\<close> \<open>mk_prop_of_term concl\<close>\<close> |
742 fun inline_assumption assumption assumption_id |
742 fun inline_assumption assumption assumption_id |
743 (VeriT_Node {id, rule, prems, proof_ctxt, concl}) = |
743 (VeriT_Node {id, rule, prems, proof_ctxt, concl}) = |
744 mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt |
744 mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt |
745 (add_assumption assumption concl) |
745 (add_assumption assumption concl) |
746 fun find_input_steps_and_inline [] = [] |
746 fun find_input_steps_and_inline [] = [] |