Lines Matching defs:gv
20 val gv = genvar (type_of x)22 EXT (GEN gv (* |- !gv. u gv =< (\x.t) gv *)23 (TRANS (SPEC gv qth)24 (SYM (BETA_CONV (mk_comb(tfun,gv)))))) end;89 val gv = genvar (type_of l)90 val pat = subst[l |-> gv] w92 ([(asl,a), (asl,subst[gv |-> r] pat)],93 fn [t1,t2] => SUBST[gv |-> SYM(MP th1 t1)] pat t2