Lines Matching defs:p2
38 let val (p1,p2) = dest_pair p
39 val t1 = PABS p2 th
43 val p2ty = type_of p2
167 (* ePBETA_CONV "(\p1.t)p2" = (|- (\p1.t)p2 = t[p2/p1]) *)
265 (* lzPBETA_CONV "(\p1.t)p2" = (|- (\p1.t)p2 = t[p2/p1]) *)
272 else let val (p1,p2) = dest_pair p
273 in [p|->v] @ (pairupvar p1 (mk_fst v)) @ (pairupvar p2 (mk_snd v)) end
364 (* PALPHA_CONV p2 "\p1. t" = (|- (\p1. t) = (\p2. t[p2/p1])) *)
374 fun new_pair p s = if is_var p then new_var p s else let val (p1,p2) = dest_pair p in mk_pair(new_pair p1 s,new_pair p2 s) end
421 (* GEN_PALPHA_CONV p2 "B p1. t" = (|- (B p1. t) = (B p2. t[p2/p1])) *)
443 val (p2,b2) = dest_pabs t2
450 else let val th1 = PALPHA_CONV p2 t1
453 TRANS th1 (PABS p2 (PALPHA b2 b1'))
1698 let val (p1,p2) = dest_pair p
1702 (P_PGEN_TAC p2)) (a,t)
2079 let val (p1,p2) = dest_pair tm
2081 mk_pair(mkfn p1 tyl, mkfn p2 tyl)