Lines Matching defs:pre
116 val pre = list_mk_star (map fst pre_post) ``:x64_set -> bool``
133 val pre = subst ss pre
135 val pre = mk_star (``zPC rip``,pre)
137 val pre = if null pre_conds then pre
138 else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds))
139 in (pre,post) end;
436 val (pre,post) = x64_pre_post g s
438 then ``SPEC_1 X64_MODEL pre {(rip,c)} post SEP_F``
439 else ``SPEC X64_MODEL pre {(rip,c)} post``
440 val tm = subst [mk_var("pre",type_of pre) |-> pre,