Lines Matching refs:xx
1081 \\ Q.PAT_X_ASSUM `MR_evl (MAP term2term (MAP SND ts),a,xx) bb` MP_TAC
1234 \\ Q.PAT_X_ASSUM `!x1 x2 x3 x4 x5. bbb ==> MR_ev (Or xx,yyy) zz` MATCH_MP_TAC
1259 \\ Q.PAT_X_ASSUM `MR_ev xx yy` MP_TAC \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases]
1295 \\ Q.PAT_X_ASSUM `MR_ev xx yy` MP_TAC
1301 \\ Q.PAT_X_ASSUM `MR_evl xx yy` MP_TAC
1316 \\ Q.PAT_X_ASSUM `MR_evl xx yy` MP_TAC
1551 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1570 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1592 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1633 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1658 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1683 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1704 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1724 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1744 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
1803 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC))
2384 \\ Q.PAT_X_ASSUM `!xx yy. bbb ==> bbbb` MP_TAC
2385 \\ Q.PAT_X_ASSUM `!xx yy. bbb ==> bbbb` (MP_TAC o Q.SPECL [`ok`,`env`])