examples/CCS/WeakEQScript.sml

106  >> REPEAT STRIP_TAC (* 2 sub-goals here *)
119  >> EQ_TAC (* 2 sub-goals here *)
124       REPEAT STRIP_TAC >- RW_TAC std_ss [] \\ (* 4 sub-goals here, first is easy *)
130       REPEAT STRIP_TAC >| (* 3 sub-goals here *)
199  >> REPEAT STRIP_TAC (* 2 sub-goals here *)
219  >> Cases_on `u` (* 2 sub-goals here *)
292  >> REPEAT STRIP_TAC (* 2 sub-goals here *)
314  >> REPEAT STRIP_TAC (* 2 sub-goals here *)
338  >> EQ_TAC (* 2 sub-goals here *)
341       IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *)
364  >> IMP_RES_TAC WEAK_TRANS_cases1 (* 2 sub-goals here *)
382  >> IMP_RES_TAC WEAK_TRANS_cases1 (* 2 sub-goals here *)
452     EPS_INDUCT_TAC (* 3 sub-goals here *)
602  >> EQ_TAC (* 2 sub-goals here *)
610       HO_MATCH_MP_TAC WEAK_EQUIV_coind \\ (* co-induction used here! *)
701  >> REPEAT STRIP_TAC (* 4 sub-goals here *)
747     EPS_INDUCT_TAC (* 3 sub-goals here *)
788  >> IMP_RES_TAC WEAK_TRANS_cases1 (* 2 sub-goals here *)
800  >> REPEAT STRIP_TAC (* 4 sub-goals here *)
802       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
824       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
844       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
856       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
876  >> REPEAT STRIP_TAC (* 4 sub-goals here *)
878       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
898       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
918       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
953  >> rpt STRIP_TAC (* 4 sub-goals here *)
955       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
971       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
987       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
1005       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
1027     EPS_INDUCT_TAC (* 3 sub-goals here *)
1030       CONJ_TAC >| (* 2 sub-goals here *)
1075  >> REPEAT STRIP_TAC (* 2 sub-goals here *)
1101  >> CONJ_TAC (* 2 sub-goals here *)
1108       REPEAT STRIP_TAC >| (* 4 sub-goals here *)
1112         IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
1117           CONJ_TAC >| (* 2 sub-goals here *)
1128           CONJ_TAC >| (* 2 sub-goals here *)
1140         IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
1145           CONJ_TAC >| (* 2 sub-goals here *)
1156           CONJ_TAC >| (* 2 sub-goals here *)
1168         IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
1174           CONJ_TAC >| (* 2 sub-goals here *)
1186           CONJ_TAC >| (* 2 sub-goals here *)
1199           CONJ_TAC >| (* 2 sub-goals here *)
1228         IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
1233           CONJ_TAC >| (* 2 sub-goals here *)
1243           CONJ_TAC >| (* 2 sub-goals here *)
1255           CONJ_TAC >| (* 2 sub-goals here *)
1310     EPS_INDUCT_TAC (* 3 sub-goals here *)
1369  >> CONJ_TAC (* 2 sub-goals here *)
1376       REPEAT STRIP_TAC >| (* 4 sub-goals here *)
1380         IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
1398         IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
1416         IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
1429         IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
1444     EPS_INDUCT_TAC (* 3 sub-goals here *)
1470     EPS_INDUCT_TAC (* 3 sub-goals here *)
1532  >> CONJ_TAC (* 2 sub-goals here *)
1539       REPEAT STRIP_TAC >| (* 4 sub-goals here *)
1551         CONJ_TAC >| (* 2 sub-goals here *)
1569         CONJ_TAC >| (* 2 sub-goals here *)
1587         CONJ_TAC >| (* 2 sub-goals here *)
1605         CONJ_TAC >| (* 2 sub-goals here *)
1669  >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *)
1670  >> REPEAT STRIP_TAC (* 2 sub-goals here *)
1700  >> IMP_RES_TAC (MATCH_MP WEAK_EQUIV_EPS (* lemma 1 used here *)
1760  >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *)
1761  >> REPEAT STRIP_TAC (* 2 sub-goals here *)
1792  >> IMP_RES_TAC (MATCH_MP STRONG_EQUIV_EPS (* lemma 1 used here *)
1796  >> IMP_RES_TAC (MATCH_MP STRONG_EQUIV_EPS (* lemma 1 used here *)