Lines Matching defs:pre
36 fun SPEC_STRENGTHEN_RULE th pre = let
37 val th = SPEC pre (MATCH_MP progTheory.SPEC_STRENGTHEN th)
241 val pre = ``aLISP1 (t1,l) * aR 1w r1 * aSTRING_SPACE r1 (LENGTH (sexp2string t1)) *
243 val (th,goal) = SPEC_STRENGTHEN_RULE th pre
302 val pre = ``pLISP1 (t1,l) * pR 1w r1 * pSTRING_SPACE r1 (LENGTH (sexp2string t1)) *
304 val (th,goal) = SPEC_STRENGTHEN_RULE th pre
346 val pre = ``xSTACK (esp-4w) [w] * xR EDI edi * xR ESP esp * xPC p``
347 val (th,goal) = SPEC_STRENGTHEN_RULE th pre
367 val pre = ``xSTACK esp [w] * ~xR EDI * xR ESP esp * xPC p``
368 val (th,goal) = SPEC_STRENGTHEN_RULE th pre
388 val pre = ``xSTACK esp [w] * ~xR EDI * xR ESP esp * xPC p``
389 val (th,goal) = SPEC_STRENGTHEN_RULE th pre
464 val pre = ``xLISP1 (t1,l) * xSTRING_SPACE w (LENGTH (sexp2string t1)) *
466 val (th,goal) = SPEC_STRENGTHEN_RULE th pre