is mentioned by

Thm* (True  P)  P	[true_imp]
Thm* (False  P)  True	[false_imp]
Thm* (P  True)  True	[imp_true]
Thm* (P  False)  P	[imp_false]
Thm* P & False  False	[and_false]
Thm* False & P  False	[false_and]
Thm* P & True  P	[and_true]
Thm* True  P  True	[true_or]
Thm* P  False  P	[or_false]
Thm* False  P  P	[false_or]
Thm* P  True  True	[or_true]
Thm* True & P  P	[true_and]
Thm* P  (f:eq('a). P)	[add_eq_pred_qf]
Thm* 'a:S, P:(eq('a)Prop). Thm* (f:eq('a). P(f))  P(<eq_pred:(x:'a. y:'a. x = y)>)	[eq_pred_unabstraction]
Thm* P:(('a'a)Prop).  Thm* P(<eq_pred:(x:'a. y:'a. x = y)>)  (f:eq('a). P(f))	[eq_pred_abstraction]
Thm* T:S, P:(TProp). (x:T. P(x))  (x:T. P(x))	[not_all]
Thm* T:S, P:(TProp). (x:T. P(x))  (x:T. P(x))	[not_exists]
Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a). Thm* iso_pair('a;'b;P;rep;abs)  Prop	[iso_pair_wf]
Thm* 'a:S, P,Q:('aProp). Thm* (x:'a. Q(x)  P(x))  (x:'a. Q(x))  P(@x:'a. Q(x))	[choose_elim_pos]
Thm* 'a:S, P,Q:('aProp). Thm* (x:'a. Q(x)  P(x)) Thm*  Thm* ((x:'a. Q(x))  (x:'a. P(x)))  P(@x:'a. Q(x))	[choose_elim_neg]
Thm* P:('aProp), x:'a. P(x)  P(@x:'a. P(x))	[choose_true]
Thm* 'a:S, P:('aProp). lem('a) = lem({x:'a| True })  'a	[lem_extensionality_axiom]
Thm* P:Prop{2}. (P)  P	[prop_to_bool_2_char]
Thm* (P)  P	[prop_to_bool_char]
Thm* P:Prop{2}. (P)	[prop_to_bool_2_wf]

In prior sections: core fun 1 well fnd int 1 bool 1

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