Lines Matching defs:inst
523 val inst = ASSUME (���^cty_REP a = ^rcl���)
532 PURE_REWRITE_RULE[SYM inst] o
534 PURE_REWRITE_RULE[inst])
953 val inst = ASSUME (���^cty_REP a = ^rcl���)
960 REWRITE_RULE[SYM inst] o
962 REWRITE_RULE[inst])
1693 val abs' = list_mk_comb(inst theta amap, Iaargs)
1698 val rep' = list_mk_comb(inst theta rmap,Irargs)
1749 val pat' = inst tytheta pat
2213 fun mk_quotient_tm (tau,ksi) = inst [alpha |-> tau, beta |-> ksi] quotient_tm
2284 val absdef = list_mk_comb(inst (map (op |->) tau_ksis) otm, xargs)
4104 in (inst tyS R, subst tmS (inst tyS x))