Lines Matching defs:imp
210 val imp = arm_print_sexp_lemma
211 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp
212 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp)
213 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp
214 val imp = RW [] imp
215 val tm = (fst o dest_imp o concl) imp
228 THEN IMP_RES_TAC (Q.INST [`w1`|->`r3`] imp)
256 THEN IMP_RES_TAC imp
271 val imp = arm_print_sexp_lemma
272 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp
273 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp)
274 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp
275 val imp = RW [] imp
276 val tm = (fst o dest_imp o concl) imp
289 THEN IMP_RES_TAC (Q.INST [`w1`|->`r3`] imp)
317 THEN IMP_RES_TAC imp
421 val imp = arm_print_sexp_lemma
422 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp
423 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp)
424 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp
425 val imp = RW [] imp
426 val tm = (fst o dest_imp o concl) imp
439 THEN IMP_RES_TAC imp
479 THEN IMP_RES_TAC imp