Def  == Unit+Unit

is mentioned by

Thm* 'a:S. (x:'a. false) = false	[ball_bfalse]
Thm* 'a:S. (x:'a. true) = true	[ball_btrue]
Thm* 'a:S. (x:'a. false) = false	[bexists_bfalse]
Thm* 'a:S. (x:'a. true) = true	[bexists_btrue]
Thm* p:. false = p  p	[equal_bfalse_to_assert_2]
Thm* p:. p = false  p	[equal_bfalse_to_assert]
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:. (bfalse) = false	[band_simp_2]
Thm* b:. (trueb) = b	[band_simp_3]
Thm* b:. (falseb) = false	[band_simp_4]
Thm* b:. (false  b) = b	[bor_simp_4]
Thm* b:. (true  b) = true	[bor_simp_3]
Thm* b:. (b  false) = b	[bor_simp_2]
Thm* b:. (b  true) = true	[bor_simp_1]
Thm* b:. (btrue) = b	[band_simp_1]
Thm* p:('a).  Thm* b_exists_unique('a;x.p(x)) Thm*  Thm* (x:'a. p(x)) & (x,y:'a. p(x) & p(y)  x = y)	[assert_of_b_exists_unique]
Def type_definition == P:'a. rep:'b'a. type_definition('a;'b;P;rep)	[htype_definition]
Def cond == b:. p:'a. q:'a. if b then p else q fi	[hcond]
Def exists_unique == p:'a. b_exists_unique('a;x.p(x))	[hexists_unique]
Def not == p:. p	[hnot]
Def or == p:. q:. p  q	[hor]
Def and == p:. q:. pq	[hand]
Def all == p:'a. x:'a. (p(x))	[hall]
Def exists == p:'a. x:'a. (p(x))	[hexists]

In prior sections: bool 1 hol hol min

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