Lines Matching defs:gv
171 val gv = genvar int_ty
173 mk_forall(gv, subst [bv |-> gv] t)
193 val gv = genvar int_ty
194 val tm1 = subst [inj_n |-> gv] tm
196 GSYM (BETA_CONV (mk_comb(mk_abs(gv,tm1), inj_n)))
392 val gv = genvar numSyntax.num
393 val newterm = mk_forall (gv, Term.subst [subtm |-> gv] tm)
421 val gv = genvar num_ty
422 val tm1 = mk_forall(gv, mk_comb (rator tm0, mk_comb(int_injection, gv)))
423 val thm1 = (* |- (!gv. P gv) = !x. 0 <= x ==> P x *)
437 val gv = genvar int_ty
439 (mk_forall(gv, subst [subtm |-> gv] tm),