hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
true
= false
False
[btrue_neq_bfalse_simp_1]
cites the following:
Thm*
true
= false
[btrue_neq_bfalse]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
Sections
HOLlib
Doc