Lines Matching defs:imp
633 val imp = PURE_ONCE_REWRITE_CONV [rw] (mk_star(frame,p))
634 val lhs = fst (dest_eq (concl imp))
743 val imp = SEP_IMP_WEAKEN c x
744 val imp = GEN v (CONV_RULE (BINOP_CONV (UNBETA_CONV v)) imp)
745 in MATCH_MP SEP_IMP_EXISTS_EXISTS imp end
756 val imp = SEP_IMP_WEAKEN (HIDE_INTRO tms) q
757 in MATCH_MP LIST_HIDE_POST_LEMMA (CONJ th imp) end
767 val imp = SEP_IMP_WEAKEN (HIDE_INTRO tms) q
768 in MATCH_MP SEP_IMP_TRANS (CONJ th imp) end