CONJ : thm -> thm -> thm

SYNOPSIS

Introduces a conjunction.

DESCRIPTION

    A1 |- t1      A2 |- t2
   ------------------------  CONJ
     A1 u A2 |- t1 /\ t2

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # CONJ (NUM_REDUCE_CONV `2 + 2`) (ASSUME `p:bool`);;
  val it : thm = p |- 2 + 2 = 4 /\ p

SEE ALSO

CONJUNCT1, CONJUNCT2, CONJUNCTS, CONJ_PAIR.