list_mk_disj : term list -> term
STRUCTURE
SYNOPSIS
Constructs the disjunction of a list of terms.
DESCRIPTION
list_mk_disj([t1,...,tn]) returns t1 \/ ... \/ tn.
FAILURE
Fails if the list is empty or if the list has more than one element, one or more of which are not of type bool.
EXAMPLE
- list_mk_disj [T,F,T];
> val it = `T \/ F \/ T` : term

- try list_mk_disj [T,mk_var("x",alpha),F];

Exception raised at boolSyntax.mk_disj:
Non-boolean argument

- list_mk_disj [mk_var("x",alpha)];
> val it = `x` : term
SEEALSO
HOL  Trindemossen-1