Lines Matching refs:here
63 >> EQ_TAC (* 2 sub-goals here *)
84 >> RES_TAC (* 2 sub-goals here *)
97 >> rpt STRIP_TAC (* 2 sub-goals here *)
261 >> rpt STRIP_TAC (* 4 sub-goals here *)
288 >> EQ_TAC (* 2 sub-goals here *)
307 >> EQ_TAC (* 2 sub-goals here *)
328 >> RES_TAC (* 4 sub-goals here *)
353 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *)
354 >> rpt STRIP_TAC (* 2 sub-goals here *)
438 >> IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_EPS (* lemma 1 used here *)
457 (MATCH_MP WEAK_BISIM_UPTO_EPS (* lemma 1 used here *)
500 >> rpt STRIP_TAC (* 4 sub-goals here *)
666 >> IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *)
681 >> IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *)
698 >> rpt STRIP_TAC (* 4 sub-goals here *)
834 >> rpt STRIP_TAC (* 2 sub-goals here *)
853 >> RES_TAC (* 2 sub-goals here *)
872 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *)
873 >> rpt STRIP_TAC (* 2 sub-goals here *)
947 >> IMP_RES_TAC (MATCH_MP OBS_BISIM_UPTO_EPS (* lemma 1 used here *)
966 (MATCH_MP OBS_BISIM_UPTO_EPS (* lemma 1 used here *)
1013 >> rpt STRIP_TAC (* 2 sub-goals here *)
1019 REWRITE_TAC [WEAK_BISIM_UPTO] >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1107 REWRITE_TAC [WEAK_BISIM_UPTO] >> rpt STRIP_TAC >| (* 4 sub-goals here *)