Lines Matching defs:ys
135 fun foo [] ys i = i
136 | foo (x::xs) ys i = let
139 in if name = new_name then foo xs (x::ys) i else let
141 in foo xs (new_var::ys) ((x |-> new_var) :: i) end end
166 val ys = (map (cdr o car) xs)
169 val frame = mk_comb(mk_comb(``aBYTE_MEMORY``,foo ys),mk_var("f",``:word32->word8``))
187 val v = hd (filter (is_var) ys @ ys)
190 val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("df",``:word32 set``))
252 val ys = (map (cdr o car) xs)
255 val frame = mk_comb(mk_comb(``aMEMORY``,foo ys),mk_var("f",``:word32->word32``))
273 val v = hd (filter (is_var) ys @ ys)
276 val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("df",``:word32 set``))