PrintForm
Definitions
Lemmas
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not
or
p
,
q
:
.
(
p
q
)
p
&
q
By:
RewriteOfThm
Thm*
p
,
q
:
.
(
p
q
) = (
p
q
) (SimpsetC [`bequal`])
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
Sections
HOLlib
Doc