Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
CONJ_PAIR : thm -> thm * thm
SYNOPSIS
Extracts both conjuncts of a conjunction.
DESCRIPTION
A |- t1 /\ t2
---------------------- CONJ_PAIR
A |- t1 A |- t2
The two resultant theorems are returned as a pair.
FAILURE CONDITIONS
Fails if the input theorem is not a conjunction.
EXAMPLE
# CONJ_PAIR(ASSUME `p /\ q`);;
val it : thm * thm = (p /\ q |- p, p /\ q |- q)