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