Def true == inl()

is mentioned by

Thm* 'a:S. (x:'a. true) = true	[ball_btrue]
Thm* 'a:S. (x:'a. true) = true	[bexists_btrue]
Thm* p:. true = p  p	[equal_btrue_to_assert_2]
Thm* p:. p = true  p	[equal_btrue_to_assert]
Thm* 'a:S, x:'a. (x = x) = true	[bequal_refl_simp]
Thm* false = true	[bnot_simp_2]
Thm* true = false	[bnot_simp_1]
Thm* b:. (trueb) = b	[band_simp_3]
Thm* b:. (true  b) = true	[bor_simp_3]
Thm* b:. (b  true) = true	[bor_simp_1]
Thm* b:. (btrue) = b	[band_simp_1]
Def t == true	[ht]

In prior sections: bool 1 hol

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