hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
p
,
q
:
.
(
p
q
)
p
&
q
[not_or]
cites the following:
Thm*
p
,
q
:
.
(
p
q
) = (
p
q
)
[bnot_thru_bor]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
Sections
HOLlib
Doc
p,q:
. 
(p 
q) 
p & qp,q:. 
(p q) = (p
q)p,q:. (p q) p & qp,q:. (p q) = (pq)