Def P  Q == PQ

is mentioned by

Thm* x,y:A, P:(AProp), i,j:. Thm* P(if i=j x else y fi)  P(if i=j x else y fi)	[eq_int_cases_test]
Thm* i,j:. (i=j) = true  i = j	[eq_int_eq_true_elim]
Thm* i,j:. (i=j) = false  i  j	[eq_int_eq_false_elim]
Thm* i,j:. i = j  (i=j) = true	[eq_int_eq_true]
Thm* i,j:. i  j  (i=j) = false	[eq_int_eq_false]
Thm* b:, x,y:T. b  if b x else y fi = x	[ite_rw_true]
Thm* b:, x,y:T. b  if b x else y fi = y	[ite_rw_false]
Thm* n:, i:{1..n}. 0 = 0 & n = 0  False	[ite_rw_test]
Thm* p,q:. pq  (p  q)	[assert_of_bimplies]
Thm* a,b:. (a  b)  a = b	[iff_imp_equal_bool]
Thm* b:. b  b = false	[not_assert_elim]
Thm* b:. b  b = true	[assert_elim]
Thm* u,v:. uv  u  v	[assert_functionality_wrt_bimplies]
Thm* u,v,w:. uv  vw  uw	[bimplies_transitivity]
Thm* u,v:. u = v  uv	[bimplies_weakening]
Thm* P:(Prop). P(false)  P(true)  (b:. P(b))	[bool_ind]

In prior sections: core well fnd int 1

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