Def P  Q == P+Q

is mentioned by

Thm* p,q:. (p  q)  p  q	[assert_of_bor]
Thm* b:. b = true  b = false	[bool_cases]

In prior sections: core

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html