dest_thm : thm -> term list * term

SYNOPSIS

Breaks a theorem into assumption list and conclusion.

DESCRIPTION

dest_thm (t1,...,tn |- t) returns ([`t1`;...;`tn`],`t`).

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # dest_thm (ASSUME `1 = 0`);;
  val it : term list * term = ([`1 = 0`], `1 = 0`)

SEE ALSO

concl, hyp.