CONJUNCT1 : thm -> thm

SYNOPSIS

Extracts left conjunct of theorem.

DESCRIPTION

    A |- t1 /\ t2
   ---------------  CONJUNCT1
       A |- t1

FAILURE CONDITIONS

Fails unless the input theorem is a conjunction.

EXAMPLE

  # CONJUNCT1(ASSUME `p /\ q`);;
  val it : thm = p /\ q |- p

SEE ALSO

CONJ_PAIR, CONJUNCT2, CONJ, CONJUNCTS.