Lines Matching refs:post
85 val post = list_mk_star (map snd pre_post) ``:x86_set -> bool``
102 val post = subst ss post
104 val post = mk_star (post,mk_comb(``xPC``,new_eip))
106 in (pre,post) end;
217 val (pre,post) = x86_pre_post g s
218 val tm = ``SPEC X86_MODEL pre {(eip,(c,w))} post``
220 mk_var("post",type_of post) |-> post,