hyp : thm -> term list

SYNOPSIS

Returns the hypotheses of a theorem.

DESCRIPTION

When applied to a theorem A |- t, the function hyp returns A, the list of hypotheses of the theorem.

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # let th = ADD_ASSUM `x = 1` (ASSUME `y = 2`);;
  val th : thm = y = 2, x = 1 |- y = 2

  # hyp th;;
  val it : term list = [`y = 2`; `x = 1`]

SEE ALSO

dest_thm, concl.