Lines Matching defs:pre
84 val pre = list_mk_star (map fst pre_post) ``:x86_set -> bool``
101 val pre = subst ss pre
103 val pre = mk_star (pre,``xPC eip``)
105 val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds))
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``
219 val tm = subst [mk_var("pre",type_of pre) |-> pre,