Lines Matching defs:pre
111 val pre = list_mk_star (map fst pre_post) ((type_of o fst o hd) pre_post)
113 val (pre,post) = if not (tmem cpsr_var (free_vars g)) then (pre,post) else let
115 in (mk_star(pre,res),mk_star(post,res)) end
139 val pre = if null pre_conds then pre else mk_cond_star(pre,mk_comb(``CONTAINER``,list_mk_conj pre_conds))
141 in (ss pre,ss code,ss post) end;
400 val pre = subst [``n:num``|->numSyntax.term_of_int n] ``aSTACK bp (l+n,ss)``
466 val (pre,code,post) = arm_pre_post s g
467 val tm = ``SPEC ARM_MODEL pre code post``
468 val tm = subst [mk_var("pre",type_of pre) |-> pre,