dest_thm : thm -> term list * term
STRUCTURE
Thm
SYNOPSIS
Breaks a theorem into assumption list and conclusion.
DESCRIPTION
dest_thm ([t1,...,tn] |- t) returns ([t1,...,tn],t).
FAILURE
Never fails.
EXAMPLE
- dest_thm (ASSUME (Term `p=T`));
> val it = ([`p = T`], `p = T`) : term list * term

SEEALSO
concl, hyp
HOL  Trindemossen-1