Def		{...i}	[int_lower]	int 1
Def		{i..j}	[int_seg]	int 1
Def		ij	[ge]	core
Def		Rem(a;n;r)	[rem_nrel]
Def		{i...}	[int_upper]	int 1
Def		Div(a;n;q)	[div_nrel]
Def		i  j < k	[lelt]	int 1
Def			[nat]	int 1
Def		AB	[le]	core
Def		P  Q	[iff]	core
Def		{T}	[guard]	core
Def		x:A. B(x)	[all]	core
Def		P  Q	[implies]	core
Def			[int_nzero]	int 1
Def		a  b	[nequal]	core
Def		Dec(P)	[decidable]	core
Def		A	[not]	core
Def			[nat_plus]	int 1
Def		i>j	[gt]	core
Def		|i|	[absval]
Def		i =  j	[pm_equal]
Def		Prop	[prop]	core
Def		imin(a;b)	[imin]
Def		a -- b	[ndiff]
Def		a mod n	[modulus]
Def		a  n	[div_floor]
Def		WellFnd{i}(A;x,y.R(x;y))	[wellfounded]	well fnd
Def		imax(a;b)	[imax]
Def		ij	[le_int]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		P  Q	[or]	core
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		i=j	[eq_int]	bool 1
Def		P  Q	[rev_implies]	core
Def		i<j	[lt_int]	bool 1
Def		b	[bnot]	bool 1

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