Def P  Q == P+Q

is mentioned by

Thm* i,j:. Thm* i<j Thm*  Thm* (F:({i..j}Prop). (k:{i..j}. F(k))  F(i)  (k:{(i+1)..j}. F(k)))	[split_int_seg_exist_dom_sfa]
Thm* k:, r1,r2:k, q1,q2:. Thm* q1k+r1 = q2k-r2  q1 = q2 & r1 = 0 & r2 = 0  q2 = q1+1 & r2 = k-r1	[division4_sfa]
Thm* a,b,c:. imin(a;b)c  ac  bc	[imin_lb]
Thm* a,b,c:. aimax(b;c)  ab  ac	[imax_ub]
Thm* i:, n:. |i|>n  i<-n  i>n	[absval_lbound]
Thm* a,b:. ab<0  a<0 & b>0  a>0 & b<0	[neg_mul_arg_bounds]
Thm* a,b:. ab>0  a>0 & b>0  a<0 & b<0	[pos_mul_arg_bounds]
Thm* a,b:. ab = 0  a = 0  b = 0	[int_entire]
Thm* a,b:. a = 0  b = 0  ab = 0	[zero_ann_a]
Def i =  j == i = j    i = -j	[pm_equal]

In prior sections: core bool 1

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