Def b == if b True else False fi

is mentioned by

Thm* b:, x,y:T. b  if b x else y fi = x	[ite_rw_true]
Thm* b:, x,y:T. b  if b x else y fi = y	[ite_rw_false]
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:. Dec(b)	[decidable__assert]
Thm* b:. b = false  b	[eqff_to_assert]
Thm* b:. b = true  b	[eqtt_to_assert]
Thm* b:. b  b = false	[not_assert_elim]
Thm* b:. b  b = true	[assert_elim]
Thm* false	[assert_of_ff]
Thm* true	[assert_of_tt]
Thm* u,v:. uv  u  v	[assert_functionality_wrt_bimplies]
Thm* u,v,w:. uv  vw  uw	[bimplies_transitivity]
Thm* u,v:. u = v  uv	[bimplies_weakening]

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