boolSyntax.dest_bool

dest_bool_case : term -> term * term * term

STRUCTURE: boolSyntax
SYNOPSIS: Destructs a case expression over bool.
DESCRIPTION: If M has the form bool_case M1 M2 b, then dest_bool_case M returns M1,M2,b.
FAILURE: Fails if M is not a full application of the bool_case constant.
SEEALSO: mk_bool_case, is_bool_case

HOL Kananaskis-13