Nuprl Theory formula_validity
(only non hidden objects are presented)
DISP
formula_valid_df
|= <F:Formula:L>== |= <F>
ABS
formula_valid
|= F ==
a:Full(F). a |= F
THM
formula_valid_wf
F:Formula. |= F
the other theories