Lines Matching defs:rep
340 fun mk_ra (b,r,rep,abs) = mk_eq(mk_abs(r,mk_eq(mk_comb(rep,mk_comb(abs,r)),r)),
342 fun mk_ar (abs,rep,a) = mk_eq(mk_abs(a,mk_comb(abs,mk_comb(rep,a))),
348 val rep = mk_var("rep",beta-->alpha)
351 val ar = ASSUME (mk_ar(abs,rep,a))
352 val ra = ASSUME (mk_ra(phi,r,rep,abs))
358 val w = mk_comb(mk_comb(tyd,phi),rep)
359 val th1 = BETA_RULE (AP_THM (AP_THM TYPE_DEFINITION phi) rep)
360 val rx' = mk_comb(rep,x')
361 val rr = mk_eq(rx',mk_comb(rep,x''))
372 val th6 = TRANS (AP_TERM rep (TRANS (AP_TERM abs xrt) xar)) th5
375 in EXISTS (mk_exists(rep,w),rep) (EQ_MP (SYM th1) (CONJ th3 th8)) end
639 val rep_name = (ns',"rep")
655 val rep = prim_new_const reptc repty
656 val ra = mk_thm([],mk_ra(phi,r,rep,abs))
659 val ar = mk_thm([],mk_ar(abs,rep,a))
670 mk_var("rep",aty-->rty)|->rep],