dest_cond : term -> term * term * term
STRUCTURE
boolSyntax
SYNOPSIS
Breaks apart a conditional into the three terms involved.
DESCRIPTION
If
M
has the form
if t then t1 else t2
then
dest_cond M
returns
(t,t1,t2)
.
FAILURE
Fails if
M
is not a conditional.
SEEALSO
mk_cond
,
is_cond
HOL
Kananaskis-14