Lines Matching defs:p2
30 let val (p1,p2) = dest_pair p
31 val t1 = PABS p2 th
35 val p2ty = type_of p2
159 (* PBETA_CONV "(\p1.t)p2" = (|- (\p1.t)p2 = t[p2/p1]) *)
174 then let val (p1,p2) = dest_pair p
179 val ((cr,rt),pr) = int_pairlike p2 x2
206 val ((cr,rt),pr) = (int_pairlike p2 x'2)
228 end (* let val (p1,p2) = ... *)
366 (* PALPHA_CONV p2 "\p1. t" = (|- (\p1. t) = (\p2. t[p2/p1])) *)
400 (* GEN_PALPHA_CONV p2 "B p1. t" = (|- (B p1. t) = (B p2. t[p2/p1])) *)
422 val (p2,b2) = dest_pabs t2
429 else let val th1 = PALPHA_CONV p2 t1
432 TRANS th1 (PABS p2 (PALPHA b2 b1'))
1675 let val (p1,p2) = dest_pair p
1679 (P_PGEN_TAC p2)) (a,t)
2058 let val (p1,p2) = dest_pair tm
2060 mk_pair(mkfn p1 tyl, mkfn p2 tyl)