bool 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* x,y:xy  xy[assert_of_le_int]
Thm* p,q:pq  (p  q)[assert_of_bimplies]
Thm* p,q:. (p  q p  q[assert_of_bor]
Thm* p,q:. (pq p & q[assert_of_band]
Thm* p:p  p[assert_of_bnot]
Thm* p,q:p=q  p = q[assert_of_eq_bool]
Thm* x,y:x=y  x = y[assert_of_eq_int_rw]
Thm* x,y:x<y  x<y[assert_of_lt_int]
Thm* x,y:Atom. x=yAtom  x  y[neg_assert_of_eq_atom]
Thm* x,y:x=y  x  y[neg_assert_of_eq_int]
Thm* x,y:x=y  x = y[assert_of_eq_int]
Thm* x,y:Atom. x=yAtom  x = y[assert_of_eq_atom]
Thm* a,b:. (a  b a = b[iff_imp_equal_bool]
Thm* b:b = false  b[eqff_to_assert]
Thm* b:b = true  b[eqtt_to_assert]

In prior sections: core well fnd int 1

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

bool 1 Sections StandardLIB Doc