Def  AB == B<A

is mentioned by

Thm*  ((a onto b))  ba	[surj_typing_imp_le]
Thm*  a,b:. ba  (Void ~ {a..b})	[intseg_void]
Thm*  b,a:. b(b -- a)+a	[ndiff_bound]
Thm*  m,k:, f:(mk). Inj(m; k; f)  mk	[inj_imp_le2]
Thm*  ((m inj k))  mk	[inj_typing_imp_le]
Thm*  (f:(mk). Inj(m; k; f))  mk	[inj_imp_le]
Thm*  a,b:. ab  (b -- a) = b-a	[ndiff_vs_diff]

In prior sections: int 1 bool 1 int 2 num thy 1 SimpleMulFacts IteratedBinops core

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