equal
deleted
inserted
replaced
714 *} |
714 *} |
715 |
715 |
716 section {* RepAbs Injection Tactic *} |
716 section {* RepAbs Injection Tactic *} |
717 |
717 |
718 (* TODO: check if it still works with first_order_match *) |
718 (* TODO: check if it still works with first_order_match *) |
719 (* FIXME/TODO: do not handle everything *)x |
719 (* FIXME/TODO: do not handle everything *) |
720 ML {* |
720 ML {* |
721 fun instantiate_tac thm = |
721 fun instantiate_tac thm = |
722 Subgoal.FOCUS (fn {concl, ...} => |
722 Subgoal.FOCUS (fn {concl, ...} => |
723 let |
723 let |
724 val pat = Drule.strip_imp_concl (cprop_of thm) |
724 val pat = Drule.strip_imp_concl (cprop_of thm) |