Lines Matching refs:here
565 >> EQ_TAC (* 2 sub-goals here *)
570 STRIP_TAC >| (* 2 sub-goals here *)
587 >> EQ_TAC (* 2 sub-goals here *)
607 IMP_RES_TAC TRANS_SUM >| (* 4 sub-goals here *)
621 IMP_RES_TAC TRANS_SUM >| (* 4 sub-goals here *)
634 >> EQ_TAC (* 2 sub-goals here *)
675 rpt GEN_TAC >> EQ_TAC (* 2 sub-goals here *)
678 IMP_RES_TAC PAR_cases >| (* 3 sub-goals here *)
710 >> IMP_RES_TAC TRANS_PAR (* 3 sub-goals here *)
741 >> EQ_TAC >| (* two goals here *)
744 IMP_RES_TAC RESTR_cases \\ (* two sub-goals here, first two steps are shared *)
751 STRIP_TAC >> art [] >| (* two sub-goals here *)
772 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
781 >> IMP_RES_TAC TRANS_RESTR (* two sub-goals here, but same proofs *)
802 rpt STRIP_TAC (* 2 goals here *)
804 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
819 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
855 >> EQ_TAC (* 2 sub-goals here *)
1252 (FN (prefix (label l) p) J = l INSERT (FN p J)) /\ (* here! *)
1257 (FN (relab p rf) J = IMAGE (REP_Relabeling rf) (FN p J)) /\ (* here *)
1269 (BN (restr L p) J = (BN p J) UNION L) /\ (* here *)