equal
deleted
inserted
replaced
104 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} => |
104 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} => |
105 (case prems of |
105 (case prems of |
106 [] => all_tac |
106 [] => all_tac |
107 | inv :: case_prems => |
107 | inv :: case_prems => |
108 let |
108 let |
109 val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv; |
109 val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv; |
110 val inv_thms = init @ [last]; |
110 val inv_thms = init @ [last]; |
111 val eqs = take e inv_thms; |
111 val eqs = take e inv_thms; |
112 fun is_local_var t = |
112 fun is_local_var t = |
113 member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t; |
113 member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t; |
114 val (eqs, assms') = |
114 val (eqs, assms') = |