Def true == inl()

is mentioned by

Thm* i,j:. (i=j) = true  i = j	[eq_int_eq_true_elim]
Thm* i,j:. i = j  (i=j) = true	[eq_int_eq_true]
Thm* b:. b = true  b	[eqtt_to_assert]
Thm* b:. b  b = true	[assert_elim]
Thm* true	[assert_of_tt]
Thm* u:. (utrue) = u	[band_tt_simp]
Thm* u:. (u  true) = true	[bor_tt_simp]
Thm* P:(Prop). P(false)  P(true)  (b:. P(b))	[bool_ind]
Thm* b:. b = true  b = false	[bool_cases]
Thm* true = false	[btrue_neq_bfalse]
Def x=yAtom == if x=yAtomtrue; false fi	[eq_atom]
Def i<j == if i<j true ; false fi	[lt_int]
Def i=j == if i=j true ; false fi	[eq_int]
Def p  q == if p true else q fi	[bor]
Def b == if b false else true fi	[bnot]

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