FDL
>
PVS
>
Prelude
>
booleans
> bool
: nonempty-type-eq-decl
bool : NONEMPTY_TYPE =
boolean