Lines Matching defs:pre
106 val pre = list_mk_star (map fst pre_post) ``:x64_set -> bool``
123 val pre = subst ss pre
125 val pre = mk_star (``zPC rip``,pre)
127 val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds))
128 in (pre,post) end;
425 val (pre,post) = x64_pre_post g s
427 then ``SPEC_1 X64_MODEL pre {(rip,c)} post SEP_F``
428 else ``SPEC X64_MODEL pre {(rip,c)} post``
429 val tm = subst [mk_var("pre",type_of pre) |-> pre,