logic/ltl/formParseScript.sml

76       rw[EQ_IMP_THM]
77       >- (rw[] >>
79       Cases_on ���px��� >> fs[] >> rw[] >>
82   simp[] >> rw[] >> Cases_on ���px��� >> simp[] >> metis_tac[]);
89   Induct_on ���s��� >> simp[token_def, TypeBase.case_eq_of ``:bool``] >> rw[] >>
90   rw[EQ_IMP_THM]
96       >- (simp[] >> Cases_on ���px��� >> fs[] >> rw[] >> metis_tac[])
97       >- (���px = []��� by (Cases_on ���px��� >> fs[] >> rw[] >> fs[]) >>
107   >- (rw[EQ_IMP_THM]
109       ������pt. px = c :: pt��� by (Cases_on ���px��� >> fs[] >> rw[] >> fs[]) >>
111   rw[EQ_IMP_THM]
184   simp[token_Spaces, BIND_DEF, token_def, literal_def] >> rw[]
191   simp[BIND_DEF, token_def, literal_def] >> rw[]
198   simp[BIND_DEF, token_def, literal_def] >> rw[]
204   simp[ES_CHOICE_DEF, BIND_DEF, token_def, literal_def] >> rw[]);
242        pairTheory.pair_case_eq, PULL_EXISTS] >> rw[] >> csimp[] >>
273   rw[Once ParseFGX_thm] >> pop_assum mp_tac >>
277   rw[]
302   ONCE_REWRITE_TAC [ParseFGX_def] >> rpt strip_tac >> rw[] >>
307   completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >>
333   rw[parseU_def, BIND_DEF] >>
350   >- (disj1_tac >> rw[] >>
376   completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >>
387   rw[]
389   fs[pairTheory.pair_case_eq] >> rw[] >>
415   rw[parseCNJ_def, BIND_DEF] >>
432   >- (disj1_tac >> rw[] >>
458   completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >>
469   rw[]
471   fs[pairTheory.pair_case_eq] >> rw[] >>
501   rw[parseDSJ_def, BIND_DEF] >>
518   >- (disj1_tac >> rw[] >>
544   completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >>
555   rw[]
557   fs[pairTheory.pair_case_eq] >> rw[] >>
587   rw[parseIMP_def, BIND_DEF] >>
604   >- (disj1_tac >> rw[] >>
630   completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >>
641   rw[]
643   fs[pairTheory.pair_case_eq] >> rw[] >>