Def b == if b True else False fi

is mentioned by

Thm* b:. b  b = false	[not_assert_imp_eq_bfalse]
Thm* b:. b  b = true	[assert_imp_eq_btrue]
Thm* p:. p  p	[not_not]
Thm* i,j:. i<j  ji	[not_lt_int]
Thm* i,j:. ij  j<i	[not_le_int]
Thm* p,q:. (p  q)  p & q	[not_or]
Thm* p,q:. (p & q)  p  q	[not_and]
Thm* A:Type, b:, x:(bA), y:((b)A). bif(b; bx.x(bx); by.y(by))  A	[bif_wf]
Thm* false  False	[assert_of_bfalse]
Thm* true  True	[assert_of_btrue]
Thm* x,y:. (x = y)  (x  y)	[assert_of_bequal_bools]
Thm* x,y:. x = y  (x  y)	[bequal_bools]
Thm* x,y:T. (x = y)  x = y	[assert_of_bequal]
Thm* P:(T). (x:T. P(x))  (x:T. P(x))	[assert_of_bexists]
Thm* P:(T). (x:T. P(x))  (x:T. P(x))	[assert_of_ball]
Thm* P:. (P) = P	[prop_to_bool_char_2]
Thm* P:Prop{2}. (P)  P	[prop_to_bool_2_char]
Thm* (P)  P	[prop_to_bool_char]
Def type_definition('a;'b;P;rep) Def == (x',x'':'b. rep(x') = rep(x'')  'a  x' = x'') Def == & (x:'a. (P(x))  (x':'b. x = rep(x')))	[type_definition]
Def x:T. P(x) == (x:T. P(x))	[bexists]
Def x:T. P(x) == (x:T. P(x))	[ball]

In prior sections: bool 1

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