Lines Matching refs:xx
1108 \\ Q.PAT_X_ASSUM `!xx.bb` (MP_TAC o Q.SPEC `t`)
1738 qpat_x_assum `mw2n (REVERSE xx) = yy` (K ALL_TAC) >>
1752 qpat_x_assum `mw2n (REVERSE xx) = yy` (K ALL_TAC) >>
2000 `!xx yy.MIN xx yy <= yy` by srw_tac[][] >>
2001 `q' <= b - 1` by METIS_TAC[] >> qpat_x_assum `!xx yy. zzz` (fn x => ALL_TAC) >>
2089 qpat_x_assum `xx DIV X2 = A` (fn x => REWRITE_TAC[x]) >>
2302 qpat_x_assum ` xx /\ (us = us) /\ yyy ==> zz` (K ALL_TAC) >>
2308 qpat_x_assum `mw2n (FRONT xx) = mw2n xx` (fn x => REWRITE_TAC[x]) >>
2410 qpat_x_assum `mw2n xx = mw2n yy - mw2n zz` (K ALL_TAC) >>
2536 qpat_x_assum `mw2n xx = mw2n yy - mw2n zz` (fn x => (
2668 \\ Q.PAT_X_ASSUM `exp = (xx,yy)` MP_TAC
3031 \\ Q.PAT_X_ASSUM `(xx,yy) = zz` (ASSUME_TAC o GSYM)