Lines Matching defs:xy
1380 let val (xy,bod) = dest_pforall tm
1381 val (x,y) = pairSyntax.dest_pair xy
1384 val th1 = RAND_CONV (PABS_CONV (UNPBETA_CONV xy)) tm
1387 val th4 = CONV_RULE (RATOR_CONV (RAND_CONV (GEN_PALPHA_CONV xy))) th3
1406 let val (xy,bod) = dest_pexists tm
1407 val (x,y) = pairSyntax.dest_pair xy
1410 val th1 = RAND_CONV (PABS_CONV (UNPBETA_CONV xy)) tm
1413 val th4 = CONV_RULE (RATOR_CONV (RAND_CONV (GEN_PALPHA_CONV xy))) th3
1433 val xy = pairSyntax.mk_pair(x,y)
1434 val result = mk_pforall (xy,bod)
1436 (UNPBETA_CONV xy))))) tm
1444 val th6 = CONV_RULE (RAND_CONV (GEN_PALPHA_CONV xy)) (TRANS th2 th5)
1460 val xy = pairSyntax.mk_pair(x,y)
1461 val result = mk_pexists (xy,bod)
1463 (UNPBETA_CONV xy))))) tm
1471 val th6 = CONV_RULE (RAND_CONV (GEN_PALPHA_CONV xy)) (TRANS th2 th5)