examples/CCS/StrongLawsScript.sml

28  >> CONJ_TAC (* 2 sub-goals here *)
37       rpt STRIP_TAC >| (* 4 sub-goals here *)
63  >> CONJ_TAC (* 2 sub-goals here *)
72       rpt STRIP_TAC >| (* 4 sub-goals here *)
97  >> CONJ_TAC (* 2 sub-goals here *)
107       rpt STRIP_TAC >| (* 4 sub-goals here *)
141  >> CONJ_TAC (* 2 sub-goals here *)
234  >> CONJ_TAC (* 2 sub-goals here *)
242       rpt STRIP_TAC >| (* 2 sub-goals here *)
251         CONJ_TAC >| (* 2 sub-goals here *)
267  >> CONJ_TAC (* 2 sub-goals here *)
274       rpt STRIP_TAC >| (* 2 sub-goals here *)
278         IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
281           CONJ_TAC >| (* 2 sub-goals here *)
297           CONJ_TAC >| (* 2 sub-goals here *)
306          IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
310            CONJ_TAC >| (* 2 sub-goals here *)
318            CONJ_TAC >| (* 2 sub-goals here *)
357       rpt STRIP_TAC >| (* 2 sub-goals here *)
365                       (ASSUME ``TRANS (par E1 E2) u E1''``)) >| (* 3 sub-goals here *)
368             CONJ_TAC >| (* 2 sub-goals here *)
377             CONJ_TAC >| (* 2 sub-goals here *)
387             CONJ_TAC >| (* 2 sub-goals here *)
408           STRIP_ASSUME_TAC (* 3 sub-goals here *)
413             CONJ_TAC >| (* 2 sub-goals here *)
437          IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
440            CONJ_TAC >| (* 2 sub-goals here *)
449            STRIP_ASSUME_TAC (* 3 sub-goals here *)
472              CONJ_TAC >| (* 2 sub-goals here *)
481            STRIP_ASSUME_TAC (* 3 sub-goals here *)
497              CONJ_TAC >| (* 2 sub-goals here *)
557         IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
626  >> CONJ_TAC (* 2 sub-goals here *)
634       rpt STRIP_TAC >| (* 4 sub-goals here *)
646         IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
699  >> CONJ_TAC (* 2 sub-goals here *)
707       rpt STRIP_TAC >| (* 4 sub-goals here *)
719         IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here, sharing end tacticals *)
735         IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
737           IMP_RES_TAC TRANS_SUM >| (* 4 sub-goals here *)
769  >> CONJ_TAC (* 2 sub-goals here *)
774       rpt STRIP_TAC >| (* 2 sub-goals here *)
793  >> rpt STRIP_TAC (* 2 sub-goals here *)
797       IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
799         IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
811         IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
825       IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
827         IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
842         IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
869  >> CONJ_TAC (* 2 sub-goals here *)
876       rpt STRIP_TAC >| (* 4 sub-goals here *)
918  >> CONJ_TAC (* 2 sub-goals here *)
925       rpt STRIP_TAC >| (* 4 sub-goals here *)
960  >> CONJ_TAC (* 2 sub-goals here *)
967       rpt STRIP_TAC >| (* 4 sub-goals here *)
979         IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *)
1010  >> CONJ_TAC (* 2 sub-goals here *)
1017       BETA_TAC >> rpt STRIP_TAC >| (* 2 sub-goals here *)
1040       IMP_RES_TAC TRANS_SUM \\ (* 2 sub-goals here, sharing initial tacticals *)
1047       IMP_RES_TAC TRANS_SUM \\(* 2 sub-goals here, sharing initial tacticals *)
1067  >> CONJ_TAC (* 2 sub-goals here *)
1114  >> CONJ_TAC (* 2 sub-goals here *)
1121       rpt STRIP_TAC >| (* 4 sub-goals here *)
1172         CONJ_TAC >| (* 2 sub-goals here *)
1186         CONJ_TAC >| (* 2 sub-goals here, first one is easy *)
1200         CONJ_TAC >| (* 2 sub-goals here, first one is easy *)
1212         CONJ_TAC >| (* 2 sub-goals here *)
1237  >> CONJ_TAC (* 2 sub-goals here *)
1252         CONJ_TAC >| (* 2 sub-goals here *)
1264         CONJ_TAC >| (* 2 sub-goals here *)
1277         CONJ_TAC >| (* 2 sub-goals here *)
1291         CONJ_TAC >| (* 2 sub-goals here, first one is easy *)
1436     Induct (* 2 sub-goals here *)
1440       EQ_TAC >| (* 2 sub-goals here *)
1451       EQ_TAC >| (* 2 sub-goals here *)
1453         STRIP_TAC >| (* 2 sub-goals here *)
1465         IMP_RES_TAC LESS_OR_EQ >| (* 2 sub-goals here *)
1488     Induct_on `m` (* 2 sub-goals here *)
1492       COND_CASES_TAC >| (* 2 sub-goals here *)
1499         >| (* 2 sub-goals here *)
1517         COND_CASES_TAC >| (* 2 sub-goals here *)
1519           EQ_TAC >| (* 2 sub-goals here *)
1544       COND_CASES_TAC >| (* 2 sub-goals here *)
1546         EQ_TAC >| (* 2 sub-goals here *)
1565           >| (* 2 sub-goals here *)
1571             IMP_RES_TAC LESS_OR_EQ >| (* 2 sub-goals here *)
1591         COND_CASES_TAC >| (* 2 sub-goals here *)
1593           EQ_TAC >| (* 2 sub-goals here *)
1596             IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
1616             IMP_RES_TAC LESS_OR_EQ >| (* 2 sub-goals here *)
1631           EQ_TAC >| (* 2 sub-goals here *)
1638             IMP_RES_TAC LESS_OR_EQ >| (* 2 sub-goals here *)
1675     Induct_on `n` (* 2 sub-goals here *)
1679       EQ_TAC >| (* 2 sub-goals here *)
1696       EQ_TAC >| (* 2 sub-goals here *)
1698         STRIP_TAC >| (* 2 sub-goals here *)
1719         IMP_RES_TAC (Q.SPECL [`k`, `SUC n`] LESS_OR_EQ) >| (* 2 sub-goals here *)
1786  >> CONJ_TAC (* 2 sub-goals here *)
1792       BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1804         IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
1866         IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
1912           CONJ_TAC >| (* 2 sub-goals here *)