Lines Matching refs:str
1266 fun ARM_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1279 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (x = Sym str) * ~(aS1 psrC) * ~(aS1 psrV)``
1281 val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm
1288 fun X86_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1303 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (x = Sym str)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF``
1305 val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm
1314 fun PPC_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1328 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (x = Sym str)) * ~(pS1 PPC_CARRY) *
1331 val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm