examples/CCS/CongruenceScript.sml

78  >> REPEAT STRIP_TAC (* 7 sub-goals here *)
149       Cases_on `p` (* 8 sub-goals here *)
163     rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *)
165                (ONCE_REWRITE_RULE [CONTEXT_cases])) (* 7 sub-goals here *)
171       Cases_on `p` (* 8 sub-goals here *)
187     rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *)
189                (ONCE_REWRITE_RULE [CONTEXT_cases])) (* 7 sub-goals here *)
195       Cases_on `p` (* 8 sub-goals here *)
219       Cases_on `p` (* 8 sub-goals here *)
243       Cases_on `p` (* 8 sub-goals here *)
276  >> REPEAT STRIP_TAC (* 6 sub-goals here *)
288  >> rpt STRIP_TAC (* 8 sub-goals here *)
322  >> Induct_on `CONTEXT` >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *)
340  >> Induct_on `CONTEXT` >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *)
398  >> rpt STRIP_TAC (* 6 sub-goals here *)
409  >> rpt STRIP_TAC (* 7 sub-goals here *)
438  >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *)
510       rpt STRIP_TAC >| (* 2 sub-goals here *)
527  >> RW_TAC std_ss [] (* 2 sub-goals here *)
530       rpt STRIP_TAC >| (* 3 sub-goals here *)
537         rpt GEN_TAC >> EQ_TAC >> rpt STRIP_TAC >> RES_TAC \\ (* 2 sub-goals here *)
643       Cases_on `p` (* 8 sub-goals here *)
657     rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *)
659                (ONCE_REWRITE_RULE [WG_cases])) (* 6 sub-goals here *)
662       Cases_on `p` (* 8 sub-goals here *)
686     rpt STRIP_TAC \\ (* 2 subgoals here, same tacticals *)
688                (ONCE_REWRITE_RULE [WG_cases])) \\ (* 6 subgoals here *)
691       Cases_on `p` (* 8 sub-goals here *)
712       Cases_on `p` (* 8 sub-goals here *)
733       Cases_on `p` (* 8 sub-goals here *)
761  >> rpt STRIP_TAC (* 6 sub-goals here *)
778  >> rpt STRIP_TAC >> RES_TAC (* 6 sub-goals here *)
827  >> rpt STRIP_TAC (* 7 sub-goals here *)
840  >> rpt STRIP_TAC (* 7 sub-goals here *)
859  >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *)
862       Cases_on `p` (* 8 or 9 sub-goals here *)
900     rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *)
901   ( POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *)
904       Cases_on `p` (* 8 or 9 sub-goals here *)
943       POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) >| (* 7 sub-goals here *)
946         Cases_on `p` (* 8 or 9 sub-goals here *)
951              (TRY (Cases_on `C'`) >> TRY (Cases_on `C`)) (* 8 or 9 sub-goals here *)
987       POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) >| (* 7 sub-goals here *)
990         Cases_on `p` (* 8 or 9 sub-goals here *)
995              Cases_on `C0` (* 8 or 9 sub-goals here *)
1034  >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *)
1037       Cases_on `p` (* 8 or 9 sub-goals here *)
1042            (TRY (Cases_on `C'`) >> TRY (Cases_on `C`)) (* 8 or 9 sub-goals here *)
1081  >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *)
1084       Cases_on `p` (* 8 or 9 sub-goals here *)
1089            Cases_on `C0` (* 8 or 9 sub-goals here *)
1153  >> rpt STRIP_TAC (* 4 sub-goals here *)
1164  >> rpt STRIP_TAC (* 3 sub-goals here *)
1181  >> Induct_on `SEQ` >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *)
1214  >> rpt STRIP_TAC (* 4 sub-goals here *)
1228  >> rpt STRIP_TAC (* 3 sub-goals here *)
1245  >> Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *)
1271  >> rpt STRIP_TAC >> FULL_SIMP_TAC std_ss []  (* 3 sub-goals here *)
1276       POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *)
1283       reverse (Cases_on `a`) >| (* 2 sub-goals here *)
1319  >> rpt STRIP_TAC >> FULL_SIMP_TAC std_ss [] (* 3 sub-goals here *)
1324       POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *)
1331       reverse (Cases_on `a`) >| (* 2 sub-goals here *)
1342       Cases_on `a1` >> Cases_on `a2` >| (* 4 sub-goals here *)
1372  >> BETA_TAC >> rpt STRIP_TAC (* 8 sub-goals here *)
1379       Induct_on `SEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1407       Induct_on `SEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1436       Induct_on `SEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1465  >> BETA_TAC >> rpt STRIP_TAC (* 14 sub-goals here *)
1472       Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1504       Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1537       Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1575       Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1615       Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1657       Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1733  >> rpt STRIP_TAC (* 6 sub-goals here *)
1756  >> rpt STRIP_TAC >> RES_TAC (* 6 sub-goals here *)