Lines Matching defs:xv
46 let val xv = variant (frees tm) xreal
66 let val (th1a, th2a) = case map (SPEC xv) [th1, th2]
70 GEN xv (tryfind (C MATCH_MP (CONJ th1a th2a)) iths)
75 GEN xv (SPECL [bod, xv] DIFF_CONST)
77 GEN xv (SPEC xv DIFF_X)
84 val th3 = UNDISCH (SPEC xv th2)
85 handle HOL_ERR _ => SPEC xv th2
91 GEN xv th7 end handle HOL_ERR _ =>
97 val th2 = GEN xv (SPEC (mk_comb(narg,xv)) th1)
99 val th4 = SPEC xv (ICONJ th2 th3)
104 GEN xv th6
109 val tm3 = mk_comb(tm2,xv)
111 GEN xv (DISCH tm3 (ASSUME tm3))