Lines Matching refs:here
61 >> REPEAT STRIP_TAC (* 4 sub-goals here, sharing initial & end tactical *)
74 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
104 >> REPEAT STRIP_TAC (* 2 sub-goals here, sharing begin & end tacticals *)
115 >> REPEAT STRIP_TAC (* 2 sub-goals here, sharing begin & end tacticals *)
164 >> Cases_on `u` (* 2 sub-goals here *)
176 IMP_RES_TAC (MATCH_MP OBS_CONGR_EPS (* lemma 1 used here *)
212 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
215 IMP_RES_TAC (MATCH_MP OBS_CONGR_WEAK_TRANS (* lemma 2 used here *)
222 IMP_RES_TAC (MATCH_MP OBS_CONGR_WEAK_TRANS (* lemma 2 used here *)
231 >> REPEAT STRIP_TAC (* 3 sub-goals here *)
252 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
284 >> rpt STRIP_TAC (* 2 sub-goals here *)
286 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
296 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
337 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
339 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
400 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
492 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
494 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
514 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
540 >> REPEAT STRIP_TAC (* 2 sub-goals here, sharing start&end tacticals *)
565 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
604 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *)
605 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
633 >> Cases_on `u` (* 2 sub-goals here *)
684 >> CONJ_TAC (* 2 sub-goals here *)