Lines Matching refs:f5
1886 \\ Q.ABBREV_TAC `f5 = (0x4w * wsp + sp - 0x4w =+ w5)
1897 (sl1 - LENGTH ss1) * ^STATIC) (fun2set (f5,df)) /\
1907 \\ Q.UNABBREV_TAC `f5`
1941 (Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC)
1950 (Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC)
1970 \\ Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC)
2048 \\ Q.ABBREV_TAC `f5 = (0x4w * wsp + sp - 0x4w =+ w5)
2059 (sl1 - LENGTH ss1) * ^STATIC) (fun2set (f5,df)) /\
2069 \\ Q.UNABBREV_TAC `f5`
2099 (Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC)
2108 (Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC)
2128 \\ Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC)