Lines Matching defs:gv
243 val gv = genvar (type_of Bvar)245 EXT (GEN gv (TRANS (TRANS (BETA_CONV (mk_comb (ufun, gv))) (SPEC gv qth))246 (SYM (BETA_CONV (mk_comb (vfun, gv))))))2538 (%gv /\ ?x. Q x) = (?x. %gv /\ Q x)2542 (%gv /\ ?P. Q P) = (?P. %gv /\ Q P)2545 %gv [%gv |-> p, Q |-> FINITE].