dest_thm

Thm.dest_thm : thm -> term list * term

Breaks a theorem into assumption list and conclusion.

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

See also

Thm.concl, Thm.hyp