mk_disj : term * term -> term
STRUCTURE
SYNOPSIS
Constructs a disjunction.
DESCRIPTION
If t1 and t2 are terms, both of type bool, then mk_disj(t1,t2) returns the term t1 \/ t2.
FAILURE
Fails if t1 or t2 does not have type bool.
SEEALSO
HOL  Trindemossen-1