IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem | Name |
Thm* a,b:. Dec(a = b) | [decidable__equal_bool] |
cites the following: |
Thm* true = false | [btrue_neq_bfalse] |
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html