The file of boolean functions defines the boolean counterparts to the usual propositional connectives, if, and, or, implies etc. We also define the boolean-valued equality function on booleans.
** Module lib_bool_funs Imports lib_bool
if = ... : {t|Type}bool->t->t->t
andalso = ... : bool->bool->bool
orelse = ... : bool->bool->bool
inv = ... : bool->bool
implies = ... : bool->bool->bool
bool_eq = ... : bool->bool->bool