Def		i  j  k	[lele]
Def		S  T	[suptype]
Def			[nat_plus]
Def		x:A. B(x)	[all]	core
Def			[int_nzero]
Def		{i...}	[int_upper]
Def		{...i}	[int_lower]
Def		{i..j}	[int_seg]
Def		Dec(P)	[decidable]	core
Def		{i...j}	[int_iseg]
Def		P  Q	[implies]	core
Def		{T}	[guard]	core
Def		P  Q	[iff]	core
Def		Prop	[prop]	core
Def			[nat]
Def		WellFnd{i}(A;x,y.R(x;y))	[wellfounded]	well fnd
Def		i  j < k	[lelt]
Def		AB	[le]	core
Def		P & Q	[and]	core
Def		a  b	[nequal]	core
Def		S  T	[subtype]	core
Def		A	[not]	core
Def		P  Q	[rev_implies]	core

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html