Lines Matching defs:pre
66 val pre = list_mk_star (map fst pre_post) ``:ppc_set -> bool``
79 val pre = subst ss pre
81 val pre = if null pre_conds then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds))
82 in (pre,post) end;
167 val (pre,post) = ppc_pre_post g
168 val tm = ``SPEC PPC_MODEL pre {(p,c)} post``
169 val tm = subst [mk_var("pre",type_of pre) |-> pre,