Def A == A  False

is mentioned by

Thm* b:. b  b = false	[not_assert_imp_eq_bfalse]
Thm* False  True	[not_false]
Thm* True  False	[not_true]
Thm* (P  False)  P	[imp_false]
Thm* p:. p  p	[not_not]
Thm* i,j:. i<j  ji	[not_lt_int]
Thm* i,j:. ij  j<i	[not_le_int]
Thm* p,q:. (p  q)  p & q	[not_or]
Thm* p,q:. (p & q)  p  q	[not_and]
Thm* T:S, P:(TProp). (x:T. P(x))  (x:T. P(x))	[not_all]
Thm* T:S, P:(TProp). (x:T. P(x))  (x:T. P(x))	[not_exists]
Thm* A:Type, b:, x:(bA), y:((b)A). bif(b; bx.x(bx); by.y(by))  A	[bif_wf]
Thm* 'a:S, P,Q:('aProp). Thm* (x:'a. Q(x)  P(x)) Thm*  Thm* ((x:'a. Q(x))  (x:'a. P(x)))  P(@x:'a. Q(x))	[choose_elim_neg]

In prior sections: core bool 1

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html