Lines Matching refs:f2
135 \\ Q.ABBREV_TAC `f2 = (r7 =+ x) ((r6 =+ h) f)`
137 one_list (r7 + 0x1w) ys r7i) (fun2set (f2,df))` by
138 (REWRITE_TAC [WORD_SUB_ADD] \\ Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC)
895 \\ Q.ABBREV_TAC `f2 = (r7 =+ w2w (0x27w:word32)) f`
901 (fun2set (f2,df))` by
902 (Q.UNABBREV_TAC `f2`
924 Q.SPECL [`T`,`p * one (r7,0x27w)`,`w1`,`w2`,`r3n`,`r7+1w`,`r8`,`h`,`f2`,`q * fr`,`c`])
1001 \\ Q.ABBREV_TAC `f2 = if b then (r7 =+ 0x28w) f else f`
1008 one_space r72 (LENGTH (s1++s3++s2++p2)) c) (fun2set (f2,df))` by
1010 \\ Q.UNABBREV_TAC `p2` \\ Q.UNABBREV_TAC `f2`
1036 one_space r72 (STRLEN s1) r73) (fun2set (f2,df))` by
1056 `r72`,`r8+8w`,`h2`,`f2`,`q * fr * one (r8,w2) * one (r8 + 0x4w,w1)`,`r73`])
1059 \\ Q.UNABBREV_TAC `f2`