bool_case : term
STRUCTURE
boolSyntax
SYNOPSIS
Constant denoting case expressions for
bool
.
LIBRARY
boolSyntax
DESCRIPTION
The ML variable
boolSyntax.bool_case
is bound to the term
bool$bool_case
.
SEEALSO
equality
,
implication
,
select
,
T
,
F
,
universal
,
existential
,
exists1
,
conjunction
,
disjunction
,
let_tm
,
arb
HOL
Kananaskis-14