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_and]
cites the following:
Thm*
p
,
q
:
.
(
p
q
) = (
p
q
)
[bnot_thru_band]
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:. (pq) = (p q)