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