IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def ![](FONT/not.png)
b == if b
false
else true
fi
is mentioned by
Thm* p: . ![](FONT/not.png) p ![](FONT/if_big.png) p | [assert_of_bnot] |
Thm* b: . b = false ![](FONT/if_big.png) ![](FONT/not.png) b | [eqff_to_assert] |
Thm* i,j: . ![](FONT/not.png) i![](FONT/le.png) j = (j< i) | [bnot_of_le_int] |
Thm* p,q: . ![](FONT/not.png) (p ![](FONT/or.png) q) = (![](FONT/not.png) p![](FONT/and.png) ![](FONT/2.png) ![](FONT/not.png) q) | [bnot_thru_bor] |
Thm* p,q: . ![](FONT/not.png) (p![](FONT/and.png) q) = (![](FONT/not.png) p ![](FONT/or.png) ![](FONT/not.png) q) | [bnot_thru_band] |
Thm* p: . ![](FONT/not.png) ![](FONT/2.png) ![](FONT/not.png) p = p | [bnot_bnot_elim] |
Def i![](FONT/le.png) j == ![](FONT/not.png) j< i | [le_int] |
Def p![](FONT/eq.png) ![](FONT/then_big.png) q == ![](FONT/not.png) p ![](FONT/or.png) q | [bimplies] |
Def p![](FONT/cpls.png) q == (p![](FONT/and.png) ![](FONT/2.png) ![](FONT/not.png) q) ![](FONT/or.png) (![](FONT/not.png) p![](FONT/and.png) q) | [bxor] |
Def p= q == (p![](FONT/and.png) q) ![](FONT/or.png) (![](FONT/not.png) p![](FONT/and.png) ![](FONT/2.png) ![](FONT/not.png) q) | [eq_bool] |
Try larger context:
StandardLIB
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html