1\DOC dest_thm
2
3\TYPE {dest_thm : thm -> term list * term}
4
5\SYNOPSIS
6Breaks a theorem into assumption list and conclusion.
7
8\DESCRIBE
9{dest_thm ([t1,...,tn] |- t)} returns {([t1,...,tn],t)}.
10
11\FAILURE
12Never fails.
13
14\EXAMPLE
15{
16- dest_thm (ASSUME (Term `p=T`));
17> val it = ([`p = T`], `p = T`) : term list * term
18}
19
20
21\SEEALSO
22Thm.concl, Thm.hyp.
23\ENDDOC
24